Transfer.lean

1import Mathlib.Topology.MetricSpace.Lipschitz2import Mathlib.Analysis.Normed.Group.Basic34/-!5# Contractive realization and fixed-point transfer67This file formalizes the transfer and order-domination statements in Section 28of `csb-BFPP-JFA.tex`. No existence assumption about a realization is discharged9here: the later construction must supply the maps and their estimates.10-/1112namespace BFPP1314set_option autoImplicit false1516universe u v1718variable {X : Type u} {D : Type v}1920/-- The fixed points of the two cyclic composites are canonically equivalent. -/21def fixedPointEquiv (A : X → D) (J : D → X) (P : D → D) :22    {x : X // J (P (A x)) = x} ≃ {z : D // A (J (P z)) = z} where23  toFun x := ⟨A x, congrArg A x.property⟩24  invFun z := ⟨J (P z), congrArg (fun w => J (P w)) z.property⟩25  left_inv x := Subtype.ext x.property26  right_inv z := Subtype.ext z.property2728theorem exists_fixedPoint_iff (A : X → D) (J : D → X) (P : D → D) :29    (∃ x, J (P (A x)) = x) ↔ ∃ z, A (J (P z)) = z := by30  constructor31  · rintro ⟨x, hx⟩32    exact ⟨A x, congrArg A hx⟩33  · rintro ⟨z, hz⟩34    exact ⟨J (P z), congrArg (fun w => J (P w)) hz⟩3536/-- The fixed-point hypothesis concerns the cyclic composite, not just `P`. -/37theorem fixedPointFree_transfer (A : X → D) (J : D → X) (P : D → D)38    (h : ∀ z, A (J (P z)) ≠ z) : ∀ x, J (P (A x)) ≠ x := by39  intro x hx40  exact h (A x) (congrArg A hx)4142/-- Order domination supplies the required fixed-point-free cyclic composite. -/43theorem order_domination [Preorder D] (A : X → D) (J : D → X) (P : D → D)44    (hAJ : ∀ z, A (J z) ≤ z) (hP : ∀ z, ¬ z ≤ P z) :45    ∀ z, A (J (P z)) ≠ z := by46  intro z hz47  apply hP z48  calc49    z = A (J (P z)) := hz.symm50    _ ≤ P z := hAJ (P z)5152theorem fixedPointFree_of_order_domination [Preorder D]53    (A : X → D) (J : D → X) (P : D → D)54    (hAJ : ∀ z, A (J z) ≤ z) (hP : ∀ z, ¬ z ≤ P z) :55    ∀ x, J (P (A x)) ≠ x :=56  fixedPointFree_transfer A J P (order_domination A J P hAJ hP)5758section Metric5960variable [PseudoMetricSpace X] [PseudoMetricSpace D]6162theorem nonexpansive_transfer (A : X → D) (J : D → X) (P : D → D)63    (hA : LipschitzWith 1 A) (hJ : LipschitzWith 1 J) (hP : LipschitzWith 1 P) :64    LipschitzWith 1 (fun x => J (P (A x))) := by65  simpa only [mul_one, Function.comp_def] using hJ.comp (hP.comp hA)6667theorem contractive_realization [Preorder D]68    (A : X → D) (J : D → X) (P : D → D)69    (hA : LipschitzWith 1 A) (hJ : LipschitzWith 1 J) (hP : LipschitzWith 1 P)70    (hAJ : ∀ z, A (J z) ≤ z) (hsub : ∀ z, ¬ z ≤ P z) :71    LipschitzWith 1 (fun x => J (P (A x))) ∧ ∀ x, J (P (A x)) ≠ x :=72  ⟨nonexpansive_transfer A J P hA hJ hP,73    fixedPointFree_of_order_domination A J P hAJ hsub⟩7475end Metric7677/-- The closed unit ball, with the metric inherited from the normed space. -/78abbrev UnitBall (X : Type u) [SeminormedAddCommGroup X] := {x : X // ‖x‖ ≤ 1}7980/-- Ball fixed point property for the given norm (the unit-ball formulation). -/81def HasBFPP (X : Type u) [SeminormedAddCommGroup X] : Prop :=82  ∀ T : UnitBall X → UnitBall X, LipschitzWith 1 T → ∃ x, T x = x8384theorem not_hasBFPP_of_fixedPointFree [SeminormedAddCommGroup X]85    (T : UnitBall X → UnitBall X) (hT : LipschitzWith 1 T)86    (hfree : ∀ x, T x ≠ x) : ¬ HasBFPP X := by87  intro h88  obtain ⟨x, hx⟩ := h T hT89  exact hfree x hx9091end BFPP

SHA-256