BallScaling.lean

1import BFPP.Transfer2import Mathlib.Analysis.Normed.Module.Basic3import Mathlib.Tactic45/-! # BFPP on the unit ball and on arbitrary nonempty closed balls -/67namespace BFPP89set_option autoImplicit false1011/-- A positive similarity transports the nonexpansive fixed point property. -/12theorem fixedPoint_property_of_similarity {X Y : Type*} [MetricSpace X] [MetricSpace Y]13    (e : X ≃ Y) (r : ℝ) (hr : 0 < r)14    (he : ∀ x y, dist (e x) (e y) = r * dist x y)15    (hX : ∀ T : X → X, LipschitzWith 1 T → ∃ x, T x = x) :16    ∀ T : Y → Y, LipschitzWith 1 T → ∃ y, T y = y := by17  intro T hT18  let S : X → X := fun x => e.symm (T (e x))19  have hS : LipschitzWith 1 S := by20    apply LipschitzWith.of_dist_le_mul21    intro x y22    simp only [NNReal.coe_one, one_mul]23    apply (mul_le_mul_iff_right₀ hr).mp24    calc25      r * dist (S x) (S y) = dist (e (S x)) (e (S y)) := (he _ _).symm26      _ = dist (T (e x)) (T (e y)) := by simp only [S, Equiv.apply_symm_apply]27      _ ≤ dist (e x) (e y) := by simpa only [NNReal.coe_one, one_mul] using hT.dist_le_mul (e x) (e y)28      _ = r * dist x y := he x y29  obtain ⟨x, hx⟩ := hX S hS30  refine ⟨e x, ?_⟩31  have hh := congrArg e hx32  simpa only [S, Equiv.apply_symm_apply] using hh3334variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]3536noncomputable def ballScaleEquiv (c : E) (r : ℝ) (hr : 0 < r) :37    UnitBall E ≃ Metric.closedBall c r where38  toFun x := ⟨c + r • x.val, by39    rw [Metric.mem_closedBall, dist_eq_norm]40    have he : c + r • x.val - c = r • x.val := by abel41    rw [he, norm_smul, Real.norm_eq_abs, abs_of_pos hr]42    exact (mul_le_mul_of_nonneg_left x.property hr.le).trans_eq (mul_one r)⟩43  invFun y := ⟨r⁻¹ • (y.val - c), by44    rw [norm_smul, Real.norm_eq_abs, abs_of_pos (inv_pos.mpr hr)]45    have hy : ‖y.val - c‖ ≤ r := by simpa only [Metric.mem_closedBall, dist_eq_norm] using y.property46    exact (mul_le_mul_of_nonneg_left hy (inv_nonneg.mpr hr.le)).trans_eq (inv_mul_cancel₀ hr.ne')⟩47  left_inv x := by48    apply Subtype.ext49    change r⁻¹ • (c + r • x.val - c) = x.val50    have he : c + r • x.val - c = r • x.val := by abel51    rw [he, smul_smul, inv_mul_cancel₀ hr.ne', one_smul]52  right_inv y := by53    apply Subtype.ext54    change c + r • (r⁻¹ • (y.val - c)) = y.val55    rw [smul_smul, mul_inv_cancel₀ hr.ne', one_smul]56    abel5758theorem ballScaleEquiv_dist (c : E) (r : ℝ) (hr : 0 < r) (x y : UnitBall E) :59    dist (ballScaleEquiv c r hr x) (ballScaleEquiv c r hr y) = r * dist x y := by60  change dist (c + r • x.val) (c + r • y.val) = r * dist x.val y.val61  rw [dist_add_left, dist_smul₀, Real.norm_eq_abs, abs_of_pos hr]6263theorem closedBall_fixedPoint_of_hasBFPP (hE : HasBFPP E) (c : E) (r : ℝ) (hr : 0 ≤ r)64    (T : Metric.closedBall c r → Metric.closedBall c r) (hT : LipschitzWith 1 T) :65    ∃ x, T x = x := by66  rcases eq_or_lt_of_le hr with hzero | hpos67  · subst r68    let x : Metric.closedBall c 0 := ⟨c, by simp⟩69    refine ⟨x, ?_⟩70    apply Subtype.ext71    exact dist_le_zero.mp (T x).property72  · exact fixedPoint_property_of_similarity (ballScaleEquiv c r hpos) r hpos73      (ballScaleEquiv_dist c r hpos) hE T hT7475/-- Radius zero is included; negative-radius balls are empty and intentionally excluded. -/76theorem hasBFPP_iff_all_closedBalls : HasBFPP E ↔77    ∀ c : E, ∀ r : ℝ, 0 ≤ r →78      ∀ T : Metric.closedBall c r → Metric.closedBall c r,79        LipschitzWith 1 T → ∃ x, T x = x := by80  refine ⟨fun h c r hr T hT => closedBall_fixedPoint_of_hasBFPP h c r hr T hT, ?_⟩81  intro h82  let e := ballScaleEquiv (0 : E) 1 (by norm_num : (0 : ℝ) < 1)83  have he : ∀ x y, dist (e.symm x) (e.symm y) = 1 * dist x y := by84    intro x y85    have hh := ballScaleEquiv_dist (0 : E) 1 (by norm_num : (0 : ℝ) < 1) (e.symm x) (e.symm y)86    change dist (e (e.symm x)) (e (e.symm y)) = 1 * dist (e.symm x) (e.symm y) at hh87    simpa only [Equiv.apply_symm_apply, one_mul] using hh.symm88  exact fixedPoint_property_of_similarity e.symm 1 (by norm_num) he (h 0 1 (by norm_num))8990theorem closedBall_negative_empty (c : E) (r : ℝ) (hr : r < 0) :91    Metric.closedBall c r = ∅ := Metric.closedBall_eq_empty.mpr hr9293end BFPP

SHA-256