InvariantIntervals.lean

1import Mathlib.Order.Zorn2import Mathlib.Order.CompleteLattice.Basic34/-! # Minimal invariant order intervals in a complete lattice -/56namespace BFPP78set_option autoImplicit false9open Set1011variable {A : Type*} [CompleteLattice A]1213def InvariantInterval (T : A → A) (s : Set A) : Prop :=14  ∃ l u, l ≤ u ∧ s = Icc l u ∧ MapsTo T s s1516theorem invariantInterval_iInter (T : A → A) (c : Set (Set A))17    (hc : ∀ s ∈ c, InvariantInterval T s) (hchain : IsChain (· ⊆ ·) c) :18    InvariantInterval T (⋂ s : c, s.val) := by19  classical20  choose l u hlu heq hT using fun s : c => hc s.val s.property21  let L := ⨆ s : c, l s22  let U := ⨅ s : c, u s23  have hcross : ∀ s t : c, l s ≤ u t := by24    intro s t25    rcases hchain.total s.property t.property with hst | hts26    · have hls : l s ∈ s.val := by rw [heq s]; exact ⟨le_rfl, hlu s⟩27      have hlt := hst hls28      rw [heq t] at hlt29      exact hlt.230    · have hut : u t ∈ t.val := by rw [heq t]; exact ⟨hlu t, le_rfl⟩31      have hus := hts hut32      rw [heq s] at hus33      exact hus.134  have hLU : L ≤ U := iSup_le (fun s => le_iInf (hcross s))35  have hI : (⋂ s : c, s.val) = Icc L U := by36    ext x37    simp only [mem_iInter, heq, mem_Icc]38    constructor39    · intro hx40      exact ⟨iSup_le (fun s => (hx s).1), le_iInf (fun s => (hx s).2)⟩41    · intro hx s42      exact ⟨(le_iSup l s).trans hx.1, hx.2.trans (iInf_le u s)⟩43  refine ⟨L, U, hLU, hI, ?_⟩44  intro x hx45  simp only [mem_iInter] at hx ⊢46  intro s47  exact hT s (hx s)4849theorem exists_minimal_invariant_interval (T : A → A) :50    ∃ l u, l ≤ u ∧ MapsTo T (Icc l u) (Icc l u) ∧51      ∀ a b, a ≤ b → Icc a b ⊆ Icc l u → MapsTo T (Icc a b) (Icc a b) →52        Icc l u ⊆ Icc a b := by53  classical54  obtain ⟨s, hs⟩ := zorn_superset {s | InvariantInterval T s} (by55    intro c hc hchain56    refine ⟨⋂ t : c, t.val, invariantInterval_iInter T c (fun t ht => hc ht) hchain, ?_⟩57    intro t ht x hx58    exact mem_iInter.mp hx ⟨t, ht⟩)59  obtain ⟨l, u, hlu, heq, hT⟩ := hs.prop60  refine ⟨l, u, hlu, heq ▸ hT, ?_⟩61  intro a b hab hsub hTab62  have hi : InvariantInterval T (Icc a b) := ⟨a, b, hab, rfl, hTab⟩63  have hrev := hs.2 hi (heq.symm ▸ hsub)64  exact heq ▸ hrev6566end BFPP

SHA-256