BanLat/OrderComplete.lean
All source files · Download exact source
SHA-256: 5e55e5876b0141ceeaa11d075b8048311eef9b5c2c314f8011e4c557f3696ff4
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Basic6import Mathlib.Order.ConditionallyCompleteLattice.Basic7import Mathlib.Data.Set.Countable89/-!10# Sigma conditional completeness1112Mathlib's `ConditionallyCompleteLattice` records Dedekind completeness of a13lattice. This file gives vector-lattice characterisations of conditional14completeness, introduces the sequential analogue15`SigmaConditionallyCompleteLattice`, and relates these completeness notions to16the Archimedean property.17-/1819open Set2021universe u2223/-! ### Shared order-completeness lemmas -/2425/-- Shift trick: in a lattice-ordered group, given a predicate `P` preserved26under pointwise transformations and a hypothesis producing a least upper bound27for `P`-sets of positive elements, the same hypothesis extends to any28`P`-set that is non-empty and bounded above. -/29private lemma exists_isLUB_of_pos_of_shift30 {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]31 {P : Set X → Prop}32 (hP_image : ∀ {S : Set X} (f : X → X), P S → P (f '' S))33 (Hpos : ∀ {S : Set X}, P S → S ⊆ {x | 0 ≤ x} → S.Nonempty → BddAbove S →34 ∃ x, IsLUB S x)35 {S : Set X} (hPS : P S) (hne : S.Nonempty) (hbdd : BddAbove S) :36 ∃ x, IsLUB S x := by37 obtain ⟨s₀, hs₀⟩ := hne38 obtain ⟨c, hc⟩ := hbdd39 have hcs₀ : s₀ ≤ c := hc hs₀40 set T : Set X := (fun x => (x - s₀)⁺) '' S with hT_def41 have hPT : P T := hP_image _ hPS42 have hTpos : T ⊆ {x | 0 ≤ x} := by43 rintro _ ⟨x, _, rfl⟩; exact posPart_nonneg _44 have hTne : T.Nonempty := ⟨_, s₀, hs₀, rfl⟩45 have hTbdd : BddAbove T := ⟨c - s₀, by46 rintro _ ⟨x, hx, rfl⟩47 calc (x - s₀)⁺ ≤ (c - s₀)⁺ := posPart_mono (sub_le_sub_right (hc hx) _)48 _ = c - s₀ := posPart_of_nonneg (sub_nonneg.mpr hcs₀)⟩49 obtain ⟨w, hw⟩ := Hpos hPT hTpos hTne hTbdd50 refine ⟨w + s₀, ?_, ?_⟩51 · intro x hx52 calc x = (x - s₀) + s₀ := by abel53 _ ≤ (x - s₀)⁺ + s₀ := by gcongr; exact le_posPart _54 _ ≤ w + s₀ := by gcongr; exact hw.1 ⟨x, hx, rfl⟩55 · intro c' hc'56 have hcs₀' : s₀ ≤ c' := hc' hs₀57 have hubT : c' - s₀ ∈ upperBounds T := by58 rintro _ ⟨x, hx, rfl⟩59 calc (x - s₀)⁺ ≤ (c' - s₀)⁺ := posPart_mono (sub_le_sub_right (hc' hx) _)60 _ = c' - s₀ := posPart_of_nonneg (sub_nonneg.mpr hcs₀')61 exact le_sub_iff_add_le.mp (hw.2 hubT)6263/-- Build a `ConditionallyCompleteLattice` structure from a blanket hypothesis64that every non-empty bounded above set has a least upper bound. -/65@[reducible]66private noncomputable def conditionallyCompleteLatticeOfHasLUB67 {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]68 (hLUB : ∀ {S : Set X}, S.Nonempty → BddAbove S → ∃ x, IsLUB S x) :69 ConditionallyCompleteLattice X := by70 classical71 have hne_neg : ∀ (s : Set X), s.Nonempty → (-s).Nonempty := fun s hne => by72 obtain ⟨x, hx⟩ := hne73 exact ⟨-x, Set.mem_neg.mpr (by rwa [neg_neg])⟩74 let sSup_fn : Set X → X := fun S =>75 if h : S.Nonempty ∧ BddAbove S then Classical.choose (hLUB h.1 h.2) else 076 exact77 { (inferInstance : Lattice X) with78 sSup := sSup_fn79 sInf := fun S => -sSup_fn (-S)80 isLUB_csSup := fun s hne hb => by81 refine ⟨?_, ?_⟩82 · intro a ha83 change a ≤ sSup_fn s84 simp only [sSup_fn, dif_pos (⟨hne, hb⟩ : s.Nonempty ∧ BddAbove s)]85 exact (Classical.choose_spec (hLUB hne hb)).1 ha86 · intro a ha87 change sSup_fn s ≤ a88 simp only [sSup_fn, dif_pos (⟨hne, ⟨a, ha⟩⟩ : s.Nonempty ∧ BddAbove s)]89 exact (Classical.choose_spec (hLUB hne ⟨a, ha⟩)).2 ha90 isGLB_csInf := fun s hne hb => by91 refine ⟨?_, ?_⟩92 · intro a ha93 change -sSup_fn (-s) ≤ a94 have hne' : (-s).Nonempty := hne_neg s hne95 have hbdd' : BddAbove (-s) := bddAbove_neg.mpr hb96 simp only [sSup_fn, dif_pos (⟨hne', hbdd'⟩ : (-s).Nonempty ∧ BddAbove (-s))]97 rw [neg_le]98 exact (Classical.choose_spec (hLUB hne' hbdd')).199 (Set.mem_neg.mpr (by rwa [neg_neg]))100 · intro a ha101 change a ≤ -sSup_fn (-s)102 have hb' : BddBelow s := ⟨a, ha⟩103 have hne' : (-s).Nonempty := hne_neg s hne104 have hbdd' : BddAbove (-s) := bddAbove_neg.mpr hb'105 simp only [sSup_fn, dif_pos (⟨hne', hbdd'⟩ : (-s).Nonempty ∧ BddAbove (-s))]106 rw [le_neg]107 apply (Classical.choose_spec (hLUB hne' hbdd')).2108 intro y hy109 rw [Set.mem_neg] at hy110 rw [le_neg]111 exact ha hy }112113/-- From the existence of a least upper bound for every increasing bounded114above net of positive elements, deduce the same conclusion for any non-empty115bounded above set of positive elements. The net is obtained by indexing over116non-empty finite subsets ordered by inclusion. -/117private lemma exists_isLUB_pos_set_of_pos_net118 {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]119 (H : ∀ {ι : Type u} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]120 {u : ι → X}, Monotone u → (∀ i, 0 ≤ u i) →121 BddAbove (range u) → ∃ x, IsLUB (range u) x)122 {S : Set X} (hpos : S ⊆ {x | 0 ≤ x}) (hne : S.Nonempty)123 (hbdd : BddAbove S) : ∃ x, IsLUB S x := by124 classical125 let ι : Type u := {F : Finset X // F.Nonempty ∧ ↑F ⊆ S}126 letI : Preorder ι := inferInstance127 letI : IsDirected ι (· ≤ ·) := ⟨fun F G =>128 ⟨⟨F.1 ∪ G.1, Finset.Nonempty.mono Finset.subset_union_left F.2.1, by129 rw [Finset.coe_union]; exact Set.union_subset F.2.2 G.2.2⟩,130 Finset.subset_union_left, Finset.subset_union_right⟩⟩131 letI : Nonempty ι := by132 obtain ⟨s₀, hs₀⟩ := hne133 exact ⟨⟨{s₀}, Finset.singleton_nonempty _, by simpa using hs₀⟩⟩134 let u : ι → X := fun F => F.1.sup' F.2.1 id135 have hmono : Monotone u := fun F G h =>136 Finset.sup'_mono id h F.2.1137 have hu_pos : ∀ F, 0 ≤ u F := fun F => by138 obtain ⟨x, hx⟩ := F.2.1139 calc (0 : X) ≤ x := hpos (F.2.2 hx)140 _ ≤ u F := Finset.le_sup' id hx141 have hu_bdd : BddAbove (range u) := by142 obtain ⟨c, hc⟩ := hbdd143 refine ⟨c, ?_⟩144 rintro _ ⟨F, rfl⟩145 refine Finset.sup'_le F.2.1 id fun i hi => hc (F.2.2 ?_)146 exact Finset.mem_coe.mpr hi147 obtain ⟨w, hw⟩ := H hmono hu_pos hu_bdd148 refine ⟨w, ?_, ?_⟩149 · intro x hx150 have hmem : u ⟨{x}, Finset.singleton_nonempty _, by simpa using hx⟩ = x := by151 simp [u, Finset.sup'_singleton]152 calc x = u ⟨{x}, Finset.singleton_nonempty _, by simpa using hx⟩ := hmem.symm153 _ ≤ w := hw.1 ⟨_, rfl⟩154 · intro c hc155 apply hw.2156 rintro _ ⟨F, rfl⟩157 refine Finset.sup'_le F.2.1 id fun i hi => hc (F.2.2 ?_)158 exact Finset.mem_coe.mpr hi159160/-! ### Characterisations of `ConditionallyCompleteLattice` -/161162/-- On a lattice-ordered additive commutative group, a163`ConditionallyCompleteLattice` structure exists provided every increasing net164of positive elements that is bounded above has a least upper bound. The net is165indexed by a type in the same universe as the carrier. -/166@[reducible]167noncomputable def conditionallyCompleteLatticeOfPosNet168 (X : Type u) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]169 (H : ∀ {ι : Type u} [Preorder ι] [IsDirected ι (· ≤ ·)] [Nonempty ι]170 {u : ι → X}, Monotone u → (∀ i, 0 ≤ u i) →171 BddAbove (range u) → ∃ x, IsLUB (range u) x) :172 ConditionallyCompleteLattice X :=173 conditionallyCompleteLatticeOfHasLUB174 (exists_isLUB_of_pos_of_shift (P := fun _ => True)175 (fun _ _ => trivial)176 (fun _ hpos hne hbdd => exists_isLUB_pos_set_of_pos_net H hpos hne hbdd)177 trivial)178179/-- On a lattice-ordered additive commutative group, a180`ConditionallyCompleteLattice` structure exists provided every non-empty181bounded above set of positive elements has a least upper bound. -/182@[reducible]183noncomputable def conditionallyCompleteLatticeOfPosSet184 (X : Type*) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]185 (H : ∀ {S : Set X}, S ⊆ {x | 0 ≤ x} → S.Nonempty → BddAbove S →186 ∃ x, IsLUB S x) :187 ConditionallyCompleteLattice X :=188 conditionallyCompleteLatticeOfHasLUB189 (exists_isLUB_of_pos_of_shift (P := fun _ => True)190 (fun _ _ => trivial) (fun _ hpos hne hbdd => H hpos hne hbdd) trivial)191192/-! ### Sigma conditional completeness -/193194/-- A lattice is **sigma conditionally complete** when non-empty bounded195countable subsets admit suprema and infima: for every countable set `s`,196`sSup s` is the least upper bound if `s` is bounded above, and `sInf s` is197the greatest lower bound if `s` is bounded below. -/198class SigmaConditionallyCompleteLattice (X : Type*)199 extends Lattice X, SupSet X, InfSet X where200 le_csSup : ∀ (s : Set X) (a : X), s.Countable → BddAbove s → a ∈ s → a ≤ sSup s201 csSup_le : ∀ (s : Set X) (a : X), s.Countable → s.Nonempty →202 a ∈ upperBounds s → sSup s ≤ a203 csInf_le : ∀ (s : Set X) (a : X), s.Countable → BddBelow s → a ∈ s → sInf s ≤ a204 le_csInf : ∀ (s : Set X) (a : X), s.Countable → s.Nonempty →205 a ∈ lowerBounds s → a ≤ sInf s206207/-- Every conditionally complete lattice is sigma conditionally complete. -/208instance (priority := 100) ConditionallyCompleteLattice.toSigmaConditionallyCompleteLattice209 {X : Type*} [ConditionallyCompleteLattice X] :210 SigmaConditionallyCompleteLattice X where211 le_csSup _ _ _ hb ha := _root_.le_csSup hb ha212 csSup_le _ _ _ hne ha := _root_.csSup_le hne ha213 csInf_le _ _ _ hb ha := _root_.csInf_le hb ha214 le_csInf _ _ _ hne ha := _root_.le_csInf hne ha215216/-! ### Characterisations of sigma conditional completeness -/217218/-- Build a `SigmaConditionallyCompleteLattice` structure from a hypothesis219that every countable non-empty bounded above set has a least upper bound. -/220@[reducible]221private noncomputable def sigmaConditionallyCompleteLatticeOfHasCountableLUB222 {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]223 (hLUB : ∀ {S : Set X}, S.Countable → S.Nonempty → BddAbove S →224 ∃ x, IsLUB S x) :225 SigmaConditionallyCompleteLattice X := by226 classical227 have hne_neg : ∀ (s : Set X), s.Nonempty → (-s).Nonempty := fun s hne => by228 obtain ⟨x, hx⟩ := hne229 exact ⟨-x, Set.mem_neg.mpr (by rwa [neg_neg])⟩230 have hcount_neg : ∀ (s : Set X), s.Countable → (-s).Countable := fun s hc => by231 have : -s = (fun x => -x) '' s := by ext; simp [Set.mem_neg]232 rw [this]; exact hc.image _233 let sSup_fn : Set X → X := fun S =>234 if h : S.Countable ∧ S.Nonempty ∧ BddAbove S235 then Classical.choose (hLUB h.1 h.2.1 h.2.2) else 0236 exact237 { (inferInstance : Lattice X) with238 sSup := sSup_fn239 sInf := fun S => -sSup_fn (-S)240 le_csSup := fun s a hc hb ha => by241 have hne : s.Nonempty := ⟨a, ha⟩242 change a ≤ sSup_fn s243 simp only [sSup_fn,244 dif_pos (⟨hc, hne, hb⟩ : s.Countable ∧ s.Nonempty ∧ BddAbove s)]245 exact (Classical.choose_spec (hLUB hc hne hb)).1 ha246 csSup_le := fun s a hc hne ha => by247 have hb : BddAbove s := ⟨a, ha⟩248 change sSup_fn s ≤ a249 simp only [sSup_fn,250 dif_pos (⟨hc, hne, hb⟩ : s.Countable ∧ s.Nonempty ∧ BddAbove s)]251 exact (Classical.choose_spec (hLUB hc hne hb)).2 ha252 csInf_le := fun s a hc hb ha => by253 change -sSup_fn (-s) ≤ a254 have hc' : (-s).Countable := hcount_neg s hc255 have hne' : (-s).Nonempty := hne_neg s ⟨a, ha⟩256 have hbdd' : BddAbove (-s) := bddAbove_neg.mpr hb257 simp only [sSup_fn,258 dif_pos (⟨hc', hne', hbdd'⟩ : (-s).Countable ∧ (-s).Nonempty ∧ BddAbove (-s))]259 rw [neg_le]260 exact (Classical.choose_spec (hLUB hc' hne' hbdd')).1261 (Set.mem_neg.mpr (by rwa [neg_neg]))262 le_csInf := fun s a hc hne ha => by263 change a ≤ -sSup_fn (-s)264 have hb : BddBelow s := ⟨a, ha⟩265 have hc' : (-s).Countable := hcount_neg s hc266 have hne' : (-s).Nonempty := hne_neg s hne267 have hbdd' : BddAbove (-s) := bddAbove_neg.mpr hb268 simp only [sSup_fn,269 dif_pos (⟨hc', hne', hbdd'⟩ : (-s).Countable ∧ (-s).Nonempty ∧ BddAbove (-s))]270 rw [le_neg]271 apply (Classical.choose_spec (hLUB hc' hne' hbdd')).2272 intro y hy273 rw [Set.mem_neg] at hy274 rw [le_neg]275 exact ha hy }276277/-- From the existence of a least upper bound for every increasing bounded278above sequence of positive elements, deduce the same conclusion for every279non-empty bounded above countable set of positive elements. The sequence is280obtained by enumerating the set and taking finite suprema. -/281private lemma exists_isLUB_pos_countable_set_of_pos_seq282 {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]283 (H : ∀ {u : ℕ → X}, Monotone u → (∀ n, 0 ≤ u n) →284 BddAbove (range u) → ∃ x, IsLUB (range u) x)285 {S : Set X} (hpos : S ⊆ {x | 0 ≤ x}) (hcount : S.Countable)286 (hne : S.Nonempty) (hbdd : BddAbove S) : ∃ x, IsLUB S x := by287 classical288 obtain ⟨g, hg⟩ := hcount.exists_eq_range hne289 let u : ℕ → X := fun n =>290 (Finset.range (n + 1)).sup' Finset.nonempty_range_add_one g291 have hg_pos : ∀ i, 0 ≤ g i := fun i => hpos (hg ▸ mem_range_self i)292 have hg_le : ∀ i c, c ∈ upperBounds S → g i ≤ c := fun i c hc =>293 hc (hg ▸ mem_range_self i)294 have hmono : Monotone u := fun m n hmn =>295 Finset.sup'_mono g (Finset.range_subset_range.mpr (Nat.succ_le_succ hmn))296 Finset.nonempty_range_add_one297 have hu_pos : ∀ n, 0 ≤ u n := fun n => by298 calc (0 : X) ≤ g 0 := hg_pos 0299 _ ≤ u n := Finset.le_sup' g (Finset.mem_range.mpr (Nat.succ_pos n))300 have hu_bdd : BddAbove (range u) := by301 obtain ⟨c, hc⟩ := hbdd302 refine ⟨c, ?_⟩303 rintro _ ⟨n, rfl⟩304 exact Finset.sup'_le _ _ fun i _ => hg_le i c hc305 obtain ⟨w, hw⟩ := H hmono hu_pos hu_bdd306 refine ⟨w, ?_, ?_⟩307 · intro x hx308 rw [hg] at hx309 obtain ⟨n, rfl⟩ := hx310 exact (Finset.le_sup' g (Finset.self_mem_range_succ n)).trans (hw.1 ⟨n, rfl⟩)311 · intro c hc312 apply hw.2313 rintro _ ⟨n, rfl⟩314 exact Finset.sup'_le _ _ fun i _ => hg_le i c hc315316/-- On a lattice-ordered additive commutative group, a `SigmaConditionallyCompleteLattice` structure317exists provided every increasing bounded above sequence of positive elements318has a least upper bound. -/319@[reducible]320noncomputable def sigmaConditionallyCompleteLatticeOfPosSeq321 (X : Type*) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]322 (H : ∀ {u : ℕ → X}, Monotone u → (∀ n, 0 ≤ u n) →323 BddAbove (range u) → ∃ x, IsLUB (range u) x) :324 SigmaConditionallyCompleteLattice X :=325 sigmaConditionallyCompleteLatticeOfHasCountableLUB326 (exists_isLUB_of_pos_of_shift (P := Set.Countable)327 (fun f hc => hc.image f)328 (fun hc hpos hne hbdd =>329 exists_isLUB_pos_countable_set_of_pos_seq H hpos hc hne hbdd))330331/-- On a lattice-ordered additive commutative group, a `SigmaConditionallyCompleteLattice` structure332exists provided every non-empty bounded above countable set of positive333elements has a least upper bound. -/334@[reducible]335noncomputable def sigmaConditionallyCompleteLatticeOfPosCountableSet336 (X : Type*) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]337 (H : ∀ {S : Set X}, S ⊆ {x | 0 ≤ x} → S.Countable → S.Nonempty →338 BddAbove S → ∃ x, IsLUB S x) :339 SigmaConditionallyCompleteLattice X :=340 sigmaConditionallyCompleteLatticeOfHasCountableLUB341 (exists_isLUB_of_pos_of_shift (P := Set.Countable)342 (fun f hc => hc.image f)343 (fun hc hpos hne hbdd => H hpos hc hne hbdd))344345/-! ### Archimedean property -/346347/-- Every sigma conditionally complete lattice-ordered group is Archimedean348in the vector-lattice sense. -/349theorem IsVLArchimedean_of_sigmaConditionallyCompleteLattice350 {X : Type*} [SigmaConditionallyCompleteLattice X] [AddCommGroup X]351 [IsOrderedAddMonoid X] : IsVLArchimedean X := by352 apply isVLArchimedean_of_eq_zero_of_nonneg_of_forall_nsmul_le353 intro x y hx hn354 set S : Set X := Set.range (fun n : ℕ => n • x) with hS_def355 have hS_count : S.Countable := Set.countable_range _356 have hS_ne : S.Nonempty := ⟨0 • x, 0, rfl⟩357 have hS_bdd : BddAbove S := ⟨y, by rintro _ ⟨n, rfl⟩; exact hn n⟩358 set u := sSup S with hu_def359 have hm : ∀ m : ℕ, m • x ≤ u := fun m =>360 SigmaConditionallyCompleteLattice.le_csSup S _ hS_count hS_bdd ⟨m, rfl⟩361 have hub : u - x ∈ upperBounds S := by362 rintro _ ⟨m, rfl⟩363 rw [le_sub_iff_add_le, ← succ_nsmul]364 exact hm (m + 1)365 have hu' : u ≤ u - x :=366 SigmaConditionallyCompleteLattice.csSup_le S _ hS_count hS_ne hub367 have hx_nonpos : x ≤ 0 := by368 have h : u + x ≤ u := le_sub_iff_add_le.mp hu'369 have h' : u + x ≤ u + 0 := by rwa [add_zero]370 exact (add_le_add_iff_left u).mp h'371 exact le_antisymm hx_nonpos hx372