Center.lean

1import Mathlib.Algebra.Order.Archimedean.Real.Basic2import Mathlib.Tactic.Linarith34/-! # The common center and sharp scalar clamp estimates -/56namespace BFPP78set_option autoImplicit false910noncomputable def commonCenter (A B : ℝ) : ℝ := (B - A) / 21112theorem commonCenter_bounds {A B : ℝ} (hA : 0 ≤ A ∧ A ≤ 2)13    (hB : 0 ≤ B ∧ B ≤ 2) (hAB : 2 ≤ A + B) :14    -1 ≤ commonCenter A B ∧ commonCenter A B ≤ 1 ∧15    1 - A ≤ commonCenter A B ∧ commonCenter A B ≤ B - 1 := by16  dsimp [commonCenter]17  obtain ⟨hA0, hA2⟩ := hA18  obtain ⟨hB0, hB2⟩ := hB19  exact ⟨by linarith, by linarith, by linarith, by linarith⟩2021theorem commonCenter_nonexpansive_bound {A B A' B' d : ℝ}22    (hA : |A - A'| ≤ d) (hB : |B - B'| ≤ d) :23    |commonCenter A B - commonCenter A' B'| ≤ d := by24  rcases abs_le.mp hA with ⟨hA₁, hA₂⟩25  rcases abs_le.mp hB with ⟨hB₁, hB₂⟩26  apply abs_le.mpr27  dsimp [commonCenter]28  exact ⟨by linarith, by linarith⟩2930theorem max_nonexpansive_bound {r s r' s' d : ℝ}31    (hr : |r - r'| ≤ d) (hs : |s - s'| ≤ d) :32    |max r s - max r' s'| ≤ d := by33  rcases abs_le.mp hr with ⟨hr₁, hr₂⟩34  rcases abs_le.mp hs with ⟨hs₁, hs₂⟩35  have h₁ : max r s ≤ max r' s' + d :=36    max_le (by linarith [le_max_left r' s']) (by linarith [le_max_right r' s'])37  have h₂ : max r' s' ≤ max r s + d :=38    max_le (by linarith [le_max_left r s]) (by linarith [le_max_right r s])39  exact abs_le.mpr ⟨by linarith, by linarith⟩4041theorem min_nonexpansive_bound {r s r' s' d : ℝ}42    (hr : |r - r'| ≤ d) (hs : |s - s'| ≤ d) :43    |min r s - min r' s'| ≤ d := by44  rcases abs_le.mp hr with ⟨hr₁, hr₂⟩45  rcases abs_le.mp hs with ⟨hs₁, hs₂⟩46  have h₁ : min r s - d ≤ min r' s' :=47    le_min (by linarith [min_le_left r s]) (by linarith [min_le_right r s])48  have h₂ : min r' s' - d ≤ min r s :=49    le_min (by linarith [min_le_left r' s']) (by linarith [min_le_right r' s'])50  exact abs_le.mpr ⟨by linarith, by linarith⟩5152theorem positive_tail_vanishes {A B : ℝ} (h : 2 ≤ A + B) :53    max (1 - A - commonCenter A B) 0 = 0 := by54  apply max_eq_right55  dsimp [commonCenter]56  linarith5758theorem negative_tail_vanishes {A B : ℝ} (h : 2 ≤ A + B) :59    max (1 - B + commonCenter A B) 0 = 0 := by60  apply max_eq_right61  dsimp [commonCenter]62  linarith6364end BFPP

SHA-256