EDSupremum.lean

1import BFPP.ContinuousBall2import Mathlib.Topology.ExtremallyDisconnected3import Mathlib.Topology.Order.Basic4import Mathlib.Topology.ContinuousMap.Algebra5import Mathlib.Topology.ContinuousMap.Ordered67/-! # Continuous lattice suprema on an extremally disconnected compact space -/89namespace BFPP1011set_option autoImplicit false12open Set TopologicalSpace1314variable {K : Type*} [TopologicalSpace K] [CompactSpace K] [ExtremallyDisconnected K]1516def edCut (S : Set (UnitBall C(K, ℝ))) (q : ℝ) : Set K :=17  closure (⋃ f : S, {t | q < f.val.val t})1819theorem edCut_isClopen (S : Set (UnitBall C(K, ℝ))) (q : ℝ) : IsClopen (edCut S q) :=20  ⟨isClosed_closure, ExtremallyDisconnected.open_closure _21    (isOpen_iUnion fun f => isOpen_lt continuous_const f.val.val.continuous)⟩2223theorem edCut_antitone (S : Set (UnitBall C(K, ℝ))) : Antitone (edCut S) := by24  intro p q hpq25  apply closure_mono26  intro t ht27  obtain ⟨f, hf⟩ := mem_iUnion.mp ht28  exact mem_iUnion.mpr ⟨f, lt_of_le_of_lt hpq hf⟩2930def edSupValues (S : Set (UnitBall C(K, ℝ))) (t : K) : Set ℝ :=31  {-1} ∪ {q | q ∈ Icc (-1) 1 ∧ t ∈ edCut S q}3233theorem edSupValues_nonempty (S : Set (UnitBall C(K, ℝ))) (t : K) :34    (edSupValues S t).Nonempty := ⟨-1, Or.inl rfl⟩3536theorem edSupValues_bddAbove (S : Set (UnitBall C(K, ℝ))) (t : K) :37    BddAbove (edSupValues S t) := by38  refine ⟨1, ?_⟩39  rintro q (hq | hq)40  · have he : q = -1 := hq41    rw [he]42    norm_num43  · exact hq.1.24445noncomputable def edSupValue (S : Set (UnitBall C(K, ℝ))) (t : K) : ℝ := sSup (edSupValues S t)4647theorem edSupValue_bounds (S : Set (UnitBall C(K, ℝ))) (t : K) :48    -1 ≤ edSupValue S t ∧ edSupValue S t ≤ 1 := by49  refine ⟨le_csSup (edSupValues_bddAbove S t) (Or.inl rfl), ?_⟩50  apply csSup_le (edSupValues_nonempty S t)51  rintro q (hq | hq)52  · have he : q = -1 := hq53    rw [he]54    norm_num55  · exact hq.1.25657theorem le_edSupValue_of_mem (S : Set (UnitBall C(K, ℝ))) (t : K) (q : ℝ)58    (hq : q ∈ Icc (-1) 1) (ht : t ∈ edCut S q) : q ≤ edSupValue S t :=59  le_csSup (edSupValues_bddAbove S t) (Or.inr ⟨hq, ht⟩)6061theorem edSupValue_le_of_not_mem (S : Set (UnitBall C(K, ℝ))) (t : K) (q : ℝ)62    (hq : -1 ≤ q) (ht : t ∉ edCut S q) : edSupValue S t ≤ q := by63  apply csSup_le (edSupValues_nonempty S t)64  rintro r (hr | hr)65  · have he : r = -1 := hr66    simpa only [he] using hq67  · by_contra h68    exact ht (edCut_antitone S (le_of_not_ge h) hr.2)6970theorem exists_cut_above_of_lt (S : Set (UnitBall C(K, ℝ))) (t : K) (a : ℝ)71    (ha : -1 ≤ a) (ht : a < edSupValue S t) :72    ∃ q, q ∈ Icc (-1) 1 ∧ a < q ∧ t ∈ edCut S q := by73  by_contra hn74  apply not_le_of_gt ht75  apply csSup_le (edSupValues_nonempty S t)76  rintro q (hq | hq)77  · have he : q = -1 := hq78    simpa only [he] using ha79  · by_contra h80    exact hn ⟨q, hq.1, lt_of_not_ge h, hq.2⟩8182theorem edSupValue_continuous (S : Set (UnitBall C(K, ℝ))) : Continuous (edSupValue S) := by83  apply OrderTopology.continuous_iff.mpr84  intro a85  constructor86  · apply isOpen_iff_mem_nhds.mpr87    intro t ht88    change a < edSupValue S t at ht89    by_cases ha : a < -190    · apply Filter.mem_of_superset Filter.univ_mem91      intro x _92      exact ha.trans_le (edSupValue_bounds S x).193    · obtain ⟨q, hq, haq, htq⟩ := exists_cut_above_of_lt S t a (le_of_not_gt ha) ht94      apply Filter.mem_of_superset ((edCut_isClopen S q).isOpen.mem_nhds htq)95      intro x hx96      exact haq.trans_le (le_edSupValue_of_mem S x q hq hx)97  · apply isOpen_iff_mem_nhds.mpr98    intro t ht99    change edSupValue S t < a at ht100    by_cases ha : 1 < a101    · apply Filter.mem_of_superset Filter.univ_mem102      intro x _103      exact (edSupValue_bounds S x).2.trans_lt ha104    · obtain ⟨q, hqt, hqa⟩ := exists_between ht105      have hq₀ : -1 ≤ q := (edSupValue_bounds S t).1.trans hqt.le106      have hq₁ : q ≤ 1 := hqa.le.trans (le_of_not_gt ha)107      have htq : t ∉ edCut S q := fun h =>108        (not_le_of_gt hqt) (le_edSupValue_of_mem S t q ⟨hq₀, hq₁⟩ h)109      apply Filter.mem_of_superset ((edCut_isClopen S q).isClosed.isOpen_compl.mem_nhds htq)110      intro x hx111      exact (edSupValue_le_of_not_mem S x q hq₀ hx).trans_lt hqa112113noncomputable def edSup (S : Set (UnitBall C(K, ℝ))) : UnitBall C(K, ℝ) :=114  ⟨⟨edSupValue S, edSupValue_continuous S⟩,115    (ContinuousMap.norm_le _ (by norm_num)).mpr (fun t => abs_le.mpr (edSupValue_bounds S t))⟩116117theorem edSup_upper (S : Set (UnitBall C(K, ℝ))) (f : UnitBall C(K, ℝ)) (hf : f ∈ S)118    (t : K) : f.val t ≤ (edSup S).val t := by119  change f.val t ≤ edSupValue S t120  by_contra hn121  obtain ⟨q, hqg, hqf⟩ := exists_between (lt_of_not_ge hn)122  have hq : q ∈ Icc (-1) 1 :=123    ⟨(edSupValue_bounds S t).1.trans hqg.le, hqf.le.trans (continuousBall_bounds f t).2⟩124  have htq : t ∈ edCut S q := subset_closure (mem_iUnion.mpr ⟨⟨f, hf⟩, hqf⟩)125  exact (not_le_of_gt hqg) (le_edSupValue_of_mem S t q hq htq)126127theorem edSup_le (S : Set (UnitBall C(K, ℝ))) (h : UnitBall C(K, ℝ))128    (hh : ∀ f ∈ S, ∀ t, f.val t ≤ h.val t) (t : K) : (edSup S).val t ≤ h.val t := by129  change edSupValue S t ≤ h.val t130  apply csSup_le (edSupValues_nonempty S t)131  rintro q (hq | hq)132  · have he : q = -1 := hq133    simpa only [he] using (continuousBall_bounds h t).1134  · have hcut : edCut S q ⊆ {x | q ≤ h.val x} := by135      apply closure_minimal136      · intro x hx137        obtain ⟨f, hf⟩ := mem_iUnion.mp hx138        exact hf.le.trans (hh f.val f.property x)139      · exact isClosed_le continuous_const h.val.continuous140    exact hcut hq.2141142theorem edSup_isLUB (S : Set (UnitBall C(K, ℝ))) : IsLUB S (edSup S) := by143  refine ⟨fun f hf t => edSup_upper S f hf t, ?_⟩144  intro h hh t145  exact edSup_le S h (fun f hf t => hh hf t) t146147@[instance_reducible] noncomputable def edBallCompleteLattice : CompleteLattice (UnitBall C(K, ℝ)) := by148  letI : SupSet (UnitBall C(K, ℝ)) := ⟨edSup⟩149  exact completeLatticeOfSup _ edSup_isLUB150151end BFPP

SHA-256