LatticeFixedPoint.lean

1import BFPP.InvariantIntervals2import Mathlib.Topology.MetricSpace.Lipschitz3import Mathlib.Tactic.Linarith45/-! # A fixed point theorem for complete lattices with interval metric balls -/67namespace BFPP89set_option autoImplicit false10open Set1112variable {A : Type*} [MetricSpace A] [CompleteLattice A]1314theorem fixedPoint_of_interval_balls15    (hballs : ∀ x : A, ∀ r : ℝ, 0 ≤ r → ∃ a b, Metric.closedBall x r = Icc a b)16    (hmid : ∀ l u : A, l ≤ u → ∃ m ∈ Icc l u, ∀ z ∈ Icc l u, dist m z ≤ dist l u / 2)17    (T : A → A) (hLip : LipschitzWith 1 T) : ∃ x, T x = x := by18  classical19  obtain ⟨l, u, hlu, hT, hmin⟩ := exists_minimal_invariant_interval T20  let M := Icc l u21  let r := dist l u / 222  have hr : 0 ≤ r := div_nonneg dist_nonneg (by norm_num)23  let N : Set A := {x | x ∈ M ∧ ∀ y ∈ M, dist x y ≤ r}24  obtain ⟨m, hmM, hm⟩ := hmid l u hlu25  have hmN : m ∈ N := ⟨hmM, hm⟩26  choose a b hab using fun y : M => hballs y.val r hr27  let L := l ⊔ ⨆ y : M, a y28  let U := u ⊓ ⨅ y : M, b y29  have hN : N = Icc L U := by30    ext x31    constructor32    · rintro ⟨hxM, hx⟩33      have hxI : ∀ y : M, x ∈ Icc (a y) (b y) := by34        intro y35        rw [← hab y]36        exact hx y.val y.property37      exact ⟨sup_le hxM.1 (iSup_le (fun y => (hxI y).1)),38        le_inf hxM.2 (le_iInf (fun y => (hxI y).2))⟩39    · intro hx40      refine ⟨⟨le_sup_left.trans hx.1, hx.2.trans inf_le_left⟩, ?_⟩41      intro y hy42      have hxI : x ∈ Icc (a ⟨y, hy⟩) (b ⟨y, hy⟩) :=43        ⟨(le_iSup a ⟨y, hy⟩).trans (le_sup_right.trans hx.1),44          (hx.2.trans inf_le_right).trans (iInf_le b ⟨y, hy⟩)⟩45      rw [← hab ⟨y, hy⟩] at hxI46      exact hxI47  have hLU : L ≤ U := by48    have hmI := hN ▸ hmN49    exact hmI.1.trans hmI.250  have hNT : MapsTo T N N := by51    intro x hx52    have hTx : T x ∈ M := hT hx.153    refine ⟨hTx, ?_⟩54    obtain ⟨a', b', hball⟩ := hballs (T x) r hr55    let p := l ⊔ a'56    let q := u ⊓ b'57    have hsub : Icc p q ⊆ M := fun z hz =>58      ⟨le_sup_left.trans hz.1, hz.2.trans inf_le_left⟩59    have hself : T x ∈ Icc a' b' := by60      rw [← hball]61      simpa using hr62    have hTxI : T x ∈ Icc p q :=63      ⟨sup_le hTx.1 hself.1, le_inf hTx.2 hself.2⟩64    have hpq : p ≤ q := hTxI.1.trans hTxI.265    have hinv : MapsTo T (Icc p q) (Icc p q) := by66      intro z hz67      have hzM := hsub hz68      have hTz := hT hzM69      have hd : dist (T z) (T x) ≤ r := by70        have hdist : dist (T z) (T x) ≤ dist z x := by71          simpa only [NNReal.coe_one, one_mul] using hLip.dist_le_mul z x72        exact hdist.trans (by simpa only [dist_comm] using hx.2 z hzM)73      have hTzI : T z ∈ Icc a' b' := by74        rw [← hball]75        exact hd76      exact ⟨sup_le hTz.1 hTzI.1, le_inf hTz.2 hTzI.2⟩77    have hMsub := hmin p q hpq hsub hinv78    intro y hy79    have hyI := hMsub hy80    have hyab : y ∈ Icc a' b' :=81      ⟨le_sup_right.trans hyI.1, hyI.2.trans inf_le_right⟩82    rw [← hball] at hyab83    simpa only [Metric.mem_closedBall, dist_comm] using hyab84  have hNM : Icc L U ⊆ Icc l u := by85    rw [← hN]86    exact fun x hx => hx.187  have hTN : MapsTo T (Icc L U) (Icc L U) := hN ▸ hNT88  have hMN : M ⊆ N := by89    rw [hN]90    exact hmin L U hLU hNM hTN91  have hlN := hMN (show l ∈ M from ⟨le_rfl, hlu⟩)92  have hdiam := hlN.2 u (show u ∈ M from ⟨hlu, le_rfl⟩)93  have heq : l = u := by94    apply dist_eq_zero.mp95    dsimp [r] at hdiam96    linarith [dist_nonneg (x := l) (y := u)]97  refine ⟨l, ?_⟩98  have hTl := hT (show l ∈ Icc l u from ⟨le_rfl, hlu⟩)99  rw [← heq] at hTl100  exact le_antisymm hTl.2 hTl.1101102end BFPP

SHA-256