BallOrderGeometry.lean

1import BFPP.ContinuousBall2import Mathlib.Topology.ContinuousMap.Ordered34/-! # Order intervals and metric balls in the continuous-function unit ball -/56namespace BFPP78set_option autoImplicit false9open Set1011variable {K : Type*} [TopologicalSpace K] [CompactSpace K]1213theorem continuousBall_dist_le_iff (f g : UnitBall C(K, ℝ)) (r : ℝ) (hr : 0 ≤ r) :14    dist f g ≤ r ↔ ∀ t, |f.val t - g.val t| ≤ r := by15  change dist f.val g.val ≤ r ↔ _16  simpa only [Real.dist_eq] using (ContinuousMap.dist_le (f := f.val) (g := g.val) hr)1718noncomputable def ballLower (f : UnitBall C(K, ℝ)) (r : ℝ) (hr : 0 ≤ r) :19    UnitBall C(K, ℝ) := by20  let g : C(K, ℝ) := ⟨fun t => max (-1) (f.val t - r), by fun_prop⟩21  refine ⟨g, (ContinuousMap.norm_le _ (by norm_num)).mpr ?_⟩22  intro t23  change |max (-1) (f.val t - r)| ≤ 124  have ht := continuousBall_bounds f t25  exact abs_le.mpr ⟨le_max_left _ _, max_le (by norm_num) (by linarith [ht.2])⟩2627noncomputable def ballUpper (f : UnitBall C(K, ℝ)) (r : ℝ) (hr : 0 ≤ r) :28    UnitBall C(K, ℝ) := by29  let g : C(K, ℝ) := ⟨fun t => min 1 (f.val t + r), by fun_prop⟩30  refine ⟨g, (ContinuousMap.norm_le _ (by norm_num)).mpr ?_⟩31  intro t32  change |min 1 (f.val t + r)| ≤ 133  have ht := continuousBall_bounds f t34  exact abs_le.mpr ⟨le_min (by norm_num) (by linarith [ht.1]), min_le_left _ _⟩3536theorem continuousBall_closedBall_eq_Icc (f : UnitBall C(K, ℝ)) (r : ℝ) (hr : 0 ≤ r) :37    Metric.closedBall f r = Icc (ballLower f r hr) (ballUpper f r hr) := by38  ext g39  simp only [Metric.mem_closedBall, continuousBall_dist_le_iff _ _ r hr, mem_Icc]40  constructor41  · intro h42    constructor <;> intro t43    · change max (-1) (f.val t - r) ≤ g.val t44      exact max_le (continuousBall_bounds g t).1 (by linarith [(abs_le.mp (h t)).1])45    · change g.val t ≤ min 1 (f.val t + r)46      exact le_min (continuousBall_bounds g t).2 (by linarith [(abs_le.mp (h t)).2])47  · intro h t48    have hlo := h.1 t49    have hup := h.2 t50    change max (-1) (f.val t - r) ≤ g.val t at hlo51    change g.val t ≤ min 1 (f.val t + r) at hup52    have hl := (le_max_right _ _).trans hlo53    have hu := hup.trans (min_le_right _ _)54    exact abs_le.mpr ⟨by linarith, by linarith⟩5556noncomputable def continuousBallMidpoint (l u : UnitBall C(K, ℝ)) : UnitBall C(K, ℝ) := by57  let m : C(K, ℝ) := ⟨fun t => (l.val t + u.val t) / 2, by fun_prop⟩58  refine ⟨m, (ContinuousMap.norm_le _ (by norm_num)).mpr ?_⟩59  intro t60  change |(l.val t + u.val t) / 2| ≤ 161  have hl := continuousBall_bounds l t62  have hu := continuousBall_bounds u t63  exact abs_le.mpr ⟨by linarith [hl.1, hu.1], by linarith [hl.2, hu.2]⟩6465theorem continuousBall_midpoint_radius (l u : UnitBall C(K, ℝ)) (hlu : l ≤ u) :66    ∃ m ∈ Icc l u, ∀ z ∈ Icc l u, dist m z ≤ dist l u / 2 := by67  refine ⟨continuousBallMidpoint l u, ?_, ?_⟩68  · constructor69    · intro t70      change l.val t ≤ (l.val t + u.val t) / 271      have ht : l.val t ≤ u.val t := hlu t72      linarith73    · intro t74      change (l.val t + u.val t) / 2 ≤ u.val t75      have ht : l.val t ≤ u.val t := hlu t76      linarith77  · intro z hz78    apply (continuousBall_dist_le_iff _ _ _ (by positivity)).mpr79    intro t80    change |(l.val t + u.val t) / 2 - z.val t| ≤ dist l u / 281    have hdist := continuousMap_abs_sub_le_dist l.val u.val t82    change |l.val t - u.val t| ≤ dist l u at hdist83    have hd := (abs_le.mp hdist).184    have hl := hz.1 t85    have hu := hz.2 t86    change l.val t ≤ z.val t at hl87    change z.val t ≤ u.val t at hu88    exact abs_le.mpr ⟨by linarith, by linarith⟩8990end BFPP

SHA-256