BanLat/Substructures/Ideal.lean
All source files · Download exact source
SHA-256: a2c95d09b57d04eb5ac12b20ae852d5e31ca35ed6437aefcccbc5a90bcd72c33
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Substructures.Sublattice6import BanLat.Normed7import BanLat.OrderUnit8import Mathlib.Analysis.Normed.Group.Completeness910/-!11# Order ideals of vector lattices1213An **order ideal** (or simply *ideal*) of a vector lattice is a sublattice that is **solid**:14if `x ∈ J` and `|y| ≤ |x|` then `y ∈ J`. Equivalently, an ideal is precisely a solid15subspace. This file defines the bundled `OrderIdeal` structure extending16`VectorSublattice` and establishes the basic characterisations and properties.17-/1819variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]20 [VectorLattice X]2122/-- An `OrderIdeal` of a vector lattice `X` is a vector sublattice that is **solid**:23whenever `x ∈ J` and `0 ≤ y ≤ x`, we have `y ∈ J`. -/24structure OrderIdeal (X : Type*) [AddCommGroup X] [Lattice X]25 [IsOrderedAddMonoid X] [VectorLattice X]26 extends VectorSublattice X where27 solid' : ∀ {x y : X}, x ∈ carrier → 0 ≤ y → y ≤ x → y ∈ carrier2829namespace OrderIdeal3031instance : SetLike (OrderIdeal X) X where32 coe J := J.carrier33 coe_injective p q h := by34 cases p; cases q; congr35 exact SetLike.ext' h3637/-- Order ideals of `X`, ordered by inclusion, form a **partial order**. -/38instance : PartialOrder (OrderIdeal X) := .ofSetLike (OrderIdeal X) X3940variable (J : OrderIdeal X)4142/-- An order ideal is solid: `x ∈ J` and `0 ≤ y ≤ x` imply `y ∈ J`. -/43theorem solid {x y : X} (hx : x ∈ J) (hy0 : 0 ≤ y) (hyx : y ≤ x) :44 y ∈ J :=45 J.solid' hx hy0 hyx4647/-- Every order ideal is a vector sublattice. -/48def toVectorSublattice' : VectorSublattice X :=49 J.toVectorSublattice5051/-- An order ideal is closed under `⊔`. -/52theorem sup_mem {x y : X} (hx : x ∈ J) (hy : y ∈ J) :53 x ⊔ y ∈ J :=54 J.toVectorSublattice.sup_mem hx hy5556/-- An order ideal is closed under `⊓`. -/57theorem inf_mem {x y : X} (hx : x ∈ J) (hy : y ∈ J) :58 x ⊓ y ∈ J :=59 J.toVectorSublattice.inf_mem hx hy6061/-- An order ideal is closed under absolute value. -/62theorem abs_mem {x : X} (hx : x ∈ J) : |x| ∈ J :=63 J.toVectorSublattice.abs_mem hx6465/-- If `|x| ∈ J` then `x ∈ J`. -/66theorem mem_of_abs_mem {x : X} (h : |x| ∈ J) : x ∈ J := by67 have hpos : x⁺ ∈ J := J.solid h (posPart_nonneg x) (sup_le (le_abs_self x) (abs_nonneg x))68 have hneg : x⁻ ∈ J := J.solid h (negPart_nonneg x) (sup_le (neg_le_abs x) (abs_nonneg x))69 have := J.toSubmodule.sub_mem hpos hneg70 rwa [posPart_sub_negPart] at this7172/-- Solidity in terms of absolute value: `x ∈ J` and `|y| ≤ |x|` imply73`y ∈ J`. -/74theorem mem_of_abs_le_abs {x y : X} (hx : x ∈ J)75 (h : |y| ≤ |x|) : y ∈ J :=76 J.mem_of_abs_mem (J.solid (J.abs_mem hx) (abs_nonneg y) h)7778/-! ### Construction from solidity -/7980/-- Build an `OrderIdeal` from a submodule that is solid in the absolute-value81sense: `x ∈ M` and `|y| ≤ |x|` imply `y ∈ M`. Every solid subspace is82automatically a sublattice and an ideal. -/83def ofSolid (M : Submodule ℝ X)84 (h : ∀ x y : X, x ∈ M → |y| ≤ |x| → y ∈ M) :85 OrderIdeal X where86 toSubmodule := M87 sup_mem' := fun {x y} hx hy => by88 have hax : |x| ∈ M := h x (|x|) hx (abs_of_nonneg (abs_nonneg x)).le89 have hay : |y| ∈ M := h y (|y|) hy (abs_of_nonneg (abs_nonneg y)).le90 have hab : |x| + |y| ∈ M := M.add_mem hax hay91 apply h (|x| + |y|) (x ⊔ y) hab92 rw [abs_of_nonneg (add_nonneg (abs_nonneg x) (abs_nonneg y))]93 apply sup_le94 · exact sup_le95 (le_trans (le_abs_self x) (le_add_of_nonneg_right (abs_nonneg y)))96 (le_trans (le_abs_self y) (le_add_of_nonneg_left (abs_nonneg x)))97 · calc -(x ⊔ y) = (-x) ⊓ (-y) := neg_sup x y98 _ ≤ -x := inf_le_left99 _ ≤ |x| := neg_le_abs x100 _ ≤ |x| + |y| := le_add_of_nonneg_right (abs_nonneg y)101 solid' := fun {x y} hx hy0 hyx =>102 h x y hx (by rwa [abs_of_nonneg hy0, abs_of_nonneg (le_trans hy0 hyx)])103104/-- A submodule is the carrier of an order ideal iff it is solid. -/105theorem solid_iff (M : Submodule ℝ X) :106 (∀ x y : X, x ∈ M → |y| ≤ |x| → y ∈ M) ↔107 (∀ x y : X, x ∈ M → 0 ≤ y → y ≤ x → y ∈ M) ∧108 ∀ x y : X, x ∈ M → y ∈ M → x ⊔ y ∈ M := by109 constructor110 · intro h111 exact ⟨fun _ _ hx hy0 hyx => (ofSolid M h).solid' hx hy0 hyx,112 fun _ _ hx hy => (ofSolid M h).sup_mem' hx hy⟩113 · intro ⟨hsol, hsup⟩ x y hx hle114 -- |x| ∈ M115 have habs_x : |x| ∈ M := hsup x (-x) hx (M.neg_mem hx)116 -- |y| ∈ M by solidity: 0 ≤ |y| ≤ |x| and |x| ∈ M117 have habs_y : |y| ∈ M := hsol (|x|) (|y|) habs_x (abs_nonneg y) hle118 -- y⁺ ∈ M: 0 ≤ y⁺ ≤ |y|119 have hpos : y⁺ ∈ M :=120 hsol (|y|) y⁺ habs_y (posPart_nonneg y) (sup_le (le_abs_self y) (abs_nonneg y))121 -- y⁻ ∈ M: 0 ≤ y⁻ ≤ |y|122 have hneg : y⁻ ∈ M :=123 hsol (|y|) y⁻ habs_y (negPart_nonneg y) (sup_le (neg_le_abs y) (abs_nonneg y))124 have := M.sub_mem hpos hneg125 rwa [posPart_sub_negPart] at this126127/-- The coercion to `Submodule ℝ X` is injective. -/128theorem toSubmodule_injective :129 Function.Injective130 (fun J : OrderIdeal X => J.toSubmodule) := by131 intro p q h132 cases p; cases q; congr133 exact VectorSublattice.toSubmodule_injective h134135/-! ### Ideal generated by a set -/136137/-- The intersection of two order ideals is an order ideal. -/138protected def inf (J₁ J₂ : OrderIdeal X) : OrderIdeal X where139 toSubmodule := J₁.toSubmodule ⊓ J₂.toSubmodule140 sup_mem' := fun hx hy =>141 ⟨J₁.sup_mem hx.1 hy.1, J₂.sup_mem hx.2 hy.2⟩142 solid' := fun hx hy0 hyx =>143 ⟨J₁.solid hx.1 hy0 hyx, J₂.solid hx.2 hy0 hyx⟩144145/-- Order ideals of `X` admit arbitrary intersections: they form a complete146semilattice for the `⊓` operation. -/147instance : InfSet (OrderIdeal X) where148 sInf S :=149 { toSubmodule := InfSet.sInf ((·.toSubmodule) '' S)150 sup_mem' := fun {x y} hx hy => by151 have hx' := (Submodule.mem_sInf).mp hx152 have hy' := (Submodule.mem_sInf).mp hy153 refine (Submodule.mem_sInf).mpr ?_154 rintro _ ⟨J, hJ, rfl⟩155 exact J.sup_mem (hx' _ ⟨J, hJ, rfl⟩) (hy' _ ⟨J, hJ, rfl⟩)156 solid' := fun {x y} hx hy0 hyx => by157 have hx' := (Submodule.mem_sInf).mp hx158 refine (Submodule.mem_sInf).mpr ?_159 rintro _ ⟨J, hJ, rfl⟩160 exact J.solid (hx' _ ⟨J, hJ, rfl⟩) hy0 hyx }161162/-- Membership in an arbitrary intersection of order ideals. -/163@[simp] theorem mem_sInf {S : Set (OrderIdeal X)} {x : X} :164 x ∈ (InfSet.sInf S : OrderIdeal X) ↔ ∀ J ∈ S, x ∈ J := by165 change x ∈ InfSet.sInf ((·.toSubmodule) '' S) ↔ _166 rw [Submodule.mem_sInf]167 exact ⟨fun h J hJ => h _ ⟨J, hJ, rfl⟩, by rintro h _ ⟨J, hJ, rfl⟩; exact h J hJ⟩168169/-- The **ideal generated by a set** `s ⊆ X` is the smallest order ideal of170`X` containing `s`, defined as the intersection of all order ideals containing171`s`. -/172def generated (s : Set X) : OrderIdeal X :=173 InfSet.sInf {J : OrderIdeal X | s ⊆ (J : Set X)}174175/-- The set `s` is contained in the ideal it generates. -/176theorem subset_generated (s : Set X) : s ⊆ (generated s : Set X) :=177 fun _ hx => mem_sInf.mpr (fun _ hJ => hJ hx)178179/-- The ideal generated by `s` is contained in any ideal containing `s`. -/180theorem generated_le {s : Set X} {J : OrderIdeal X} (h : s ⊆ (J : Set X)) :181 generated s ≤ J :=182 fun _ hx => mem_sInf.mp hx J h183184/-- The order ideal of elements bounded in absolute value by a non-negative185linear combination of `|y|`'s for `y ∈ s`. -/186private def generatedAux (s : Set X) : OrderIdeal X :=187 ofSolid188 { carrier := {x : X | ∃ (t : Finset X) (c : X → ℝ),189 (∀ y ∈ t, y ∈ s) ∧ (∀ y ∈ t, 0 ≤ c y) ∧ |x| ≤ ∑ y ∈ t, c y • |y|}190 add_mem' := by191 classical192 rintro x x' ⟨t, c, hts, hc, hxle⟩ ⟨t', c', ht's, hc', hx'le⟩193 refine ⟨t ∪ t',194 fun y => (if y ∈ t then c y else 0) + (if y ∈ t' then c' y else 0),195 ?_, ?_, ?_⟩196 · intro y hy197 rcases Finset.mem_union.mp hy with h | h198 · exact hts y h199 · exact ht's y h200 · intro y _201 refine add_nonneg ?_ ?_202 · split_ifs with h203 · exact hc y h204 · exact le_rfl205 · split_ifs with h206 · exact hc' y h207 · exact le_rfl208 · have h1 : ∑ y ∈ t, c y • |y| =209 ∑ y ∈ t ∪ t', (if y ∈ t then c y else 0) • |y| := by210 rw [show ∑ y ∈ t, c y • |y| =211 ∑ y ∈ t, (if y ∈ t then c y else 0) • |y| from212 Finset.sum_congr rfl (fun y hy => by rw [if_pos hy])]213 exact Finset.sum_subset Finset.subset_union_left214 (fun y _ hy => by rw [if_neg hy, zero_smul])215 have h2 : ∑ y ∈ t', c' y • |y| =216 ∑ y ∈ t ∪ t', (if y ∈ t' then c' y else 0) • |y| := by217 rw [show ∑ y ∈ t', c' y • |y| =218 ∑ y ∈ t', (if y ∈ t' then c' y else 0) • |y| from219 Finset.sum_congr rfl (fun y hy => by rw [if_pos hy])]220 exact Finset.sum_subset Finset.subset_union_right221 (fun y _ hy => by rw [if_neg hy, zero_smul])222 calc |x + x'|223 ≤ |x| + |x'| := abs_add_le _ _224 _ ≤ (∑ y ∈ t, c y • |y|) + (∑ y ∈ t', c' y • |y|) :=225 add_le_add hxle hx'le226 _ = (∑ y ∈ t ∪ t', (if y ∈ t then c y else 0) • |y|) +227 (∑ y ∈ t ∪ t', (if y ∈ t' then c' y else 0) • |y|) := by228 rw [h1, h2]229 _ = ∑ y ∈ t ∪ t', ((if y ∈ t then c y else 0) +230 (if y ∈ t' then c' y else 0)) • |y| := by231 rw [← Finset.sum_add_distrib]232 refine Finset.sum_congr rfl fun y _ => ?_233 rw [add_smul]234 zero_mem' := ⟨∅, fun _ => 0, by simp, by simp, by simp⟩235 smul_mem' := by236 rintro r x ⟨t, c, hts, hc, hxle⟩237 refine ⟨t, fun y => |r| * c y, hts,238 fun y hy => mul_nonneg (abs_nonneg _) (hc y hy), ?_⟩239 rw [abs_smul']240 calc |r| • |x|241 ≤ |r| • ∑ y ∈ t, c y • |y| :=242 smul_le_smul_of_nonneg_left hxle (abs_nonneg _)243 _ = ∑ y ∈ t, (|r| * c y) • |y| := by244 rw [Finset.smul_sum]245 refine Finset.sum_congr rfl fun y _ => ?_246 rw [smul_smul] }247 (fun x y ⟨t, c, hts, hc, hxle⟩ hyx_abs =>248 ⟨t, c, hts, hc, le_trans hyx_abs hxle⟩)249250/-- **Explicit description of the generated ideal.** An element `x` lies in the251ideal generated by `s` if and only if `|x|` is bounded above by a non-negative252linear combination of absolute values of elements of `s`. -/253theorem mem_generated_iff {s : Set X} {x : X} :254 x ∈ generated s ↔255 ∃ (t : Finset X) (c : X → ℝ),256 (∀ y ∈ t, y ∈ s) ∧ (∀ y ∈ t, 0 ≤ c y) ∧257 |x| ≤ ∑ y ∈ t, c y • |y| := by258 refine ⟨fun hx => ?_, ?_⟩259 · have h : generated s ≤ generatedAux s := by260 apply generated_le261 intro y hy262 exact ⟨{y}, fun _ => 1, by263 intro z hz; rw [Finset.mem_singleton] at hz; exact hz ▸ hy,264 by intros; exact zero_le_one,265 by simp⟩266 exact h hx267 · rintro ⟨t, c, hts, hc, hxle⟩268 refine mem_sInf.mpr fun J hJ => ?_269 have hsum : ∑ y ∈ t, c y • |y| ∈ J := by270 apply J.toSubmodule.sum_mem271 intro y hy272 exact J.toSubmodule.smul_mem _ (J.abs_mem (hJ (hts y hy)))273 exact J.mem_of_abs_mem (J.solid hsum (abs_nonneg _) hxle)274275/-! ### Principal ideal -/276277/-- The **principal ideal** generated by `a` is the set of elements `x` with278`|x| ≤ c • |a|` for some `c ≥ 0`. -/279def principal (a : X) : OrderIdeal X where280 toSubmodule :=281 { carrier := {x : X | ∃ c : ℝ, 0 ≤ c ∧ |x| ≤ c • |a|}282 add_mem' := fun {x y} ⟨cx, hcx, hx⟩ ⟨cy, hcy, hy⟩ =>283 ⟨cx + cy, add_nonneg hcx hcy, by284 calc |x + y| ≤ |x| + |y| := abs_add_le x y285 _ ≤ cx • |a| + cy • |a| := add_le_add hx hy286 _ = (cx + cy) • |a| := (add_smul cx cy |a|).symm⟩287 zero_mem' := ⟨0, le_rfl, by simp⟩288 smul_mem' := fun r x ⟨c, hc, hx⟩ =>289 ⟨|r| * c, mul_nonneg (abs_nonneg r) hc, by290 rw [abs_smul' x r]291 calc |r| • |x| ≤ |r| • (c • |a|) :=292 smul_le_smul_of_nonneg_left hx (abs_nonneg r)293 _ = (|r| * c) • |a| := smul_smul |r| c |a|⟩ }294 sup_mem' := fun {x y} ⟨cx, hcx, hx⟩ ⟨cy, hcy, hy⟩ =>295 ⟨cx + cy, add_nonneg hcx hcy, by296 have : |x ⊔ y| ≤ |x| + |y| := by297 apply sup_le298 · exact sup_le299 (le_trans (le_abs_self x) (le_add_of_nonneg_right (abs_nonneg y)))300 (le_trans (le_abs_self y) (le_add_of_nonneg_left (abs_nonneg x)))301 · calc -(x ⊔ y) = (-x) ⊓ (-y) := neg_sup x y302 _ ≤ -x := inf_le_left303 _ ≤ |x| := neg_le_abs x304 _ ≤ |x| + |y| := le_add_of_nonneg_right (abs_nonneg y)305 calc |x ⊔ y| ≤ |x| + |y| := this306 _ ≤ cx • |a| + cy • |a| := add_le_add hx hy307 _ = (cx + cy) • |a| := (add_smul cx cy |a|).symm⟩308 solid' := fun {x y} ⟨c, hc, hx⟩ hy0 hyx =>309 ⟨c, hc, le_trans (by rw [abs_of_nonneg hy0]; exact le_trans hyx (le_abs_self x)) hx⟩310311/-- Characterisation of membership in the principal ideal. -/312theorem mem_principal {a x : X} :313 x ∈ principal a ↔ ∃ c : ℝ, 0 ≤ c ∧ |x| ≤ c • |a| := Iff.rfl314315/-- The generator belongs to its own principal ideal. -/316theorem self_mem_principal (a : X) : a ∈ principal a :=317 ⟨1, zero_le_one, by simp⟩318319/-- The principal ideal generated by `a` coincides with the ideal generated by320the singleton `{|a|}`. -/321theorem principal_eq_generated_abs (a : X) :322 principal a = generated ({|a|} : Set X) := by323 refine le_antisymm (fun x hx => ?_) (generated_le ?_)324 · obtain ⟨c, hc, hxle⟩ := hx325 refine mem_sInf.mpr fun J hJ => ?_326 have ha : |a| ∈ J := hJ rfl327 have hca : c • |a| ∈ J := J.toSubmodule.smul_mem c ha328 exact J.mem_of_abs_mem (J.solid hca (abs_nonneg _) hxle)329 · intro y hy330 rw [Set.mem_singleton_iff] at hy331 subst hy332 exact ⟨1, zero_le_one, by rw [abs_abs, one_smul]⟩333334/-! ### Gauge norm on the principal ideal -/335336variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]337 [VectorLattice X]338339/-- The **gauge norm** (or order-unit norm) of `x` with respect to `a` is340`inf {c ≥ 0 | |x| ≤ c • |a|}`. For `x` in the principal ideal of `a`, this341is finite and defines a lattice seminorm; it is a norm precisely when the342ambient space is Archimedean. -/343noncomputable def gaugeNorm (a x : X) : ℝ :=344 sInf {c : ℝ | 0 ≤ c ∧ |x| ≤ c • |a|}345346variable (a : X)347348/-- The gauge norm is non-negative. -/349theorem gaugeNorm_nonneg (x : X) : 0 ≤ gaugeNorm a x := by350 unfold gaugeNorm351 by_cases h : {c : ℝ | 0 ≤ c ∧ |x| ≤ c • |a|}.Nonempty352 · exact le_csInf h fun _ ⟨hc, _⟩ => hc353 · rw [Set.not_nonempty_iff_eq_empty.mp h, Real.sInf_empty]354355/-- The gauge norm of zero is zero. -/356theorem gaugeNorm_zero : gaugeNorm a 0 = 0 := by357 apply le_antisymm358 · exact csInf_le ⟨0, fun _ ⟨hd, _⟩ => hd⟩ ⟨le_rfl, by simp⟩359 · exact gaugeNorm_nonneg a 0360361/-- The gauge norm is symmetric. -/362theorem gaugeNorm_neg (x : X) :363 gaugeNorm a (-x) = gaugeNorm a x := by364 simp only [gaugeNorm, abs_neg]365366/-- Triangle inequality for the gauge norm. -/367private theorem gaugeNorm_bddBelow (x : X) :368 BddBelow {c : ℝ | 0 ≤ c ∧ |x| ≤ c • |a|} :=369 ⟨0, fun _ ⟨hc, _⟩ => hc⟩370371theorem gaugeNorm_add_le {x y : X} (hx : x ∈ principal a) (hy : y ∈ principal a) :372 gaugeNorm a (x + y) ≤ gaugeNorm a x + gaugeNorm a y := by373 -- Bound `gaugeNorm a (x + y) - cy` for each admissible bound `cy` of `y`.374 have step1 : ∀ cy, cy ∈ {c : ℝ | 0 ≤ c ∧ |y| ≤ c • |a|} →375 gaugeNorm a (x + y) - cy ≤ gaugeNorm a x := by376 intro cy ⟨hcy, hcy_le⟩377 apply le_csInf hx378 intro cx ⟨hcx, hcx_le⟩379 have : cx + cy ∈ {c : ℝ | 0 ≤ c ∧ |x + y| ≤ c • |a|} :=380 ⟨add_nonneg hcx hcy, le_trans (abs_add_le x y)381 (by rw [add_smul]; exact add_le_add hcx_le hcy_le)⟩382 exact sub_le_iff_le_add.mpr (csInf_le (gaugeNorm_bddBelow a (x + y)) this)383 -- Then take the infimum over admissible bounds of `y`.384 have step2 : gaugeNorm a (x + y) - gaugeNorm a x ≤ gaugeNorm a y :=385 le_csInf hy (fun cy hcy => by linarith [step1 cy hcy])386 linarith387388/-- Absolute homogeneity of the gauge norm. -/389private theorem gaugeNorm_div_mem {r : ℝ} (hr_pos : 0 < |r|) {x : X} {c : ℝ}390 (hc : 0 ≤ c) (hle : |r| • |x| ≤ c • |a|) :391 c / |r| ∈ {c : ℝ | 0 ≤ c ∧ |x| ≤ c • |a|} := by392 refine ⟨div_nonneg hc hr_pos.le, ?_⟩393 have := smul_le_smul_of_nonneg_left hle (inv_nonneg.mpr hr_pos.le)394 rw [smul_smul, inv_mul_cancel₀ (ne_of_gt hr_pos), one_smul, smul_smul] at this395 rwa [div_eq_inv_mul]396397theorem gaugeNorm_smul (r : ℝ) (x : X) :398 gaugeNorm a (r • x) = |r| * gaugeNorm a x := by399 by_cases hr : r = 0400 · simp [hr, gaugeNorm_zero]401 · have hr_pos : (0 : ℝ) < |r| := abs_pos.mpr hr402 -- S_x nonempty ↔ S_{rx} nonempty (when r ≠ 0)403 by_cases hne : {c : ℝ | 0 ≤ c ∧ |x| ≤ c • |a|}.Nonempty404 · apply le_antisymm405 · -- ≤: gaugeNorm(rx)/|r| ≤ gaugeNorm(x), then multiply406 suffices h : gaugeNorm a (r • x) / |r| ≤ gaugeNorm a x from407 (div_le_iff₀ hr_pos).mp h |>.trans (le_of_eq (mul_comm _ _))408 apply le_csInf hne409 intro d ⟨hd, hle⟩410 rw [div_le_iff₀ hr_pos]411 exact (csInf_le (gaugeNorm_bddBelow a (r • x))412 ⟨mul_nonneg hr_pos.le hd, by413 rw [abs_smul' x r, mul_smul]414 exact smul_le_smul_of_nonneg_left hle hr_pos.le⟩).trans (le_of_eq (mul_comm _ _))415 · -- ≥: for any c in S_{rx}, c/|r| ∈ S_x, so gaugeNorm(x) ≤ c/|r|416 obtain ⟨d, hd, hle⟩ := hne417 have hne_rx : {c : ℝ | 0 ≤ c ∧ |r • x| ≤ c • |a|}.Nonempty :=418 ⟨|r| * d, mul_nonneg hr_pos.le hd, by419 rw [abs_smul' x r, mul_smul]420 exact smul_le_smul_of_nonneg_left hle hr_pos.le⟩421 apply le_csInf hne_rx422 intro c ⟨hc, hle'⟩423 calc |r| * gaugeNorm a x424 ≤ |r| * (c / |r|) :=425 mul_le_mul_of_nonneg_left426 (csInf_le (gaugeNorm_bddBelow a x) (gaugeNorm_div_mem a hr_pos hc427 (by rwa [abs_smul' x r] at hle'))) hr_pos.le428 _ = c := by field_simp429 · -- Both S_x and S_{rx} empty: both sides are 0430 have hne2 : ¬{c : ℝ | 0 ≤ c ∧ |r • x| ≤ c • |a|}.Nonempty := by431 intro ⟨c, hc, hle⟩432 exact hne ⟨c / |r|, gaugeNorm_div_mem a hr_pos hc433 (by rwa [abs_smul' x r] at hle)⟩434 simp only [gaugeNorm, Set.not_nonempty_iff_eq_empty.mp hne,435 Set.not_nonempty_iff_eq_empty.mp hne2, Real.sInf_empty, mul_zero]436437/-- The gauge norm controls the absolute value: `|x| ≤ ‖x‖_a • |a|` for438`x` in the principal ideal. -/439theorem abs_le_gaugeNorm_smul_abs [IsVLArchimedean X] {x : X}440 (hx : x ∈ principal a) : |x| ≤ gaugeNorm a x • |a| := by441 suffices h : (|x| - gaugeNorm a x • |a|)⁺ = 0 by442 have := le_posPart (|x| - gaugeNorm a x • |a|)443 rw [h] at this; exact sub_nonpos.mp this444 apply IsVLArchimedean.eq_zero_of_nonneg_of_forall_nsmul_le (y := |a|) (posPart_nonneg _)445 intro n446 by_cases hn : n = 0447 · simp [hn]448 · have hne : {c : ℝ | 0 ≤ c ∧ |x| ≤ c • |a|}.Nonempty := hx449 have hn_pos : (0 : ℝ) < ↑n := Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)450 have hlt : gaugeNorm a x < gaugeNorm a x + 1 / ↑n :=451 lt_add_of_pos_right _ (div_pos one_pos hn_pos)452 obtain ⟨c, ⟨_, hcle⟩, hc_lt⟩ := exists_lt_of_csInf_lt hne hlt453 have hstep : |x| - gaugeNorm a x • |a| ≤ (1 / (↑n : ℝ)) • |a| := by454 calc |x| - gaugeNorm a x • |a|455 ≤ c • |a| - gaugeNorm a x • |a| := sub_le_sub_right hcle _456 _ = (c - gaugeNorm a x) • |a| := (sub_smul c (gaugeNorm a x) |a|).symm457 _ ≤ (1 / ↑n) • |a| :=458 smul_le_smul_of_nonneg_right (by linarith) (abs_nonneg a)459 have hpos_le : (|x| - gaugeNorm a x • |a|)⁺ ≤ (1 / (↑n : ℝ)) • |a| :=460 sup_le hstep (smul_nonneg (div_nonneg one_pos.le hn_pos.le) (abs_nonneg a))461 calc n • (|x| - gaugeNorm a x • |a|)⁺462 ≤ n • ((1 / (↑n : ℝ)) • |a|) :=463 nsmul_le_nsmul hpos_le (smul_nonneg (div_nonneg one_pos.le hn_pos.le)464 (abs_nonneg a)) le_rfl465 _ = ((↑n : ℝ) * (1 / ↑n)) • |a| := by466 rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul]467 _ = |a| := by rw [mul_one_div_cancel (ne_of_gt hn_pos), one_smul]468469/-- Any admissible constant bounds the gauge norm from above. -/470theorem gaugeNorm_le_of_abs_le {x : X} {c : ℝ} (hc : 0 ≤ c)471 (h : |x| ≤ c • |a|) : gaugeNorm a x ≤ c :=472 csInf_le ⟨0, fun _ ⟨hd, _⟩ => hd⟩ ⟨hc, h⟩473474/-- The gauge norm is monotone with respect to `|·|`: the solid-norm475property. -/476theorem gaugeNorm_mono_abs {x y : X} (hy : y ∈ principal a) (h : |x| ≤ |y|) :477 gaugeNorm a x ≤ gaugeNorm a y := by478 -- S_y ⊆ S_x, so sInf S_x ≤ sInf S_y479 apply le_csInf hy480 intro c ⟨hc, hle⟩481 exact csInf_le (gaugeNorm_bddBelow a x) ⟨hc, le_trans h hle⟩482483/-- In an Archimedean vector lattice the gauge norm is definite:484`gaugeNorm a x = 0 ↔ x = 0` for `x` in the principal ideal of `a`. -/485theorem gaugeNorm_eq_zero_iff [IsVLArchimedean X] {x : X}486 (hx : x ∈ principal a) : gaugeNorm a x = 0 ↔ x = 0 := by487 constructor488 · intro h489 have := abs_le_gaugeNorm_smul_abs a hx490 rw [h, zero_smul] at this491 exact (abs_eq_zero_iff_zero x).mp (le_antisymm this (abs_nonneg x))492 · intro h; rw [h]; exact gaugeNorm_zero a493494/-- The closed unit ball of the gauge norm is the order interval495`[-|a|, |a|]`. -/496theorem gaugeNorm_le_one_iff [IsVLArchimedean X] {x : X} (hx : x ∈ principal a) :497 gaugeNorm a x ≤ 1 ↔ |x| ≤ |a| := by498 constructor499 · intro h500 calc |x| ≤ gaugeNorm a x • |a| := abs_le_gaugeNorm_smul_abs a hx501 _ ≤ 1 • |a| := smul_le_smul_of_nonneg_right h (abs_nonneg a)502 _ = |a| := one_smul ℝ |a|503 · intro h504 exact gaugeNorm_le_of_abs_le a one_pos.le (by rwa [one_smul])505506/-- If `0 ≤ e ≤ u` then `‖·‖_u ≤ ‖·‖_e` on `I_e`. -/507theorem gaugeNorm_anti {e u : X} (he : 0 ≤ e) (heu : e ≤ u)508 {x : X} (hx : x ∈ principal e) : gaugeNorm u x ≤ gaugeNorm e x := by509 -- S_e ⊆ S_u (since |e| = e ≤ u = |u|, so c • |e| ≤ c • |u|)510 apply le_csInf hx511 intro c ⟨hc, hle⟩512 apply csInf_le (gaugeNorm_bddBelow u x)513 exact ⟨hc, le_trans hle (smul_le_smul_of_nonneg_left514 (by rwa [abs_of_nonneg he, abs_of_nonneg (le_trans he heu)]) hc)⟩515516/-! ### Normed vector lattice structure on the principal ideal -/517518/-- The underlying submodule of the principal ideal. -/519abbrev principalSubmodule (a : X) : Submodule ℝ X :=520 (principal a).toSubmodule521522/-- The gauge norm as a `Norm` instance on the principal ideal. -/523noncomputable instance instNormPrincipal (a : X) :524 Norm ↥(principalSubmodule a) where525 norm x := gaugeNorm a x.1526527/-- The principal ideal inherits a lattice structure from `X`. -/528noncomputable instance instLatticePrincipal (a : X) :529 Lattice ↥(principalSubmodule a) where530 sup x y := ⟨x.1 ⊔ y.1, (principal a).sup_mem x.2 y.2⟩531 inf x y := ⟨x.1 ⊓ y.1, (principal a).inf_mem x.2 y.2⟩532 le_sup_left := fun x y => show x.1 ≤ x.1 ⊔ y.1 from le_sup_left533 le_sup_right := fun x y => show y.1 ≤ x.1 ⊔ y.1 from le_sup_right534 sup_le := fun x y z h1 h2 => show x.1 ⊔ y.1 ≤ z.1 from sup_le h1 h2535 inf_le_left := fun x y => show x.1 ⊓ y.1 ≤ x.1 from inf_le_left536 inf_le_right := fun x y => show x.1 ⊓ y.1 ≤ y.1 from inf_le_right537 le_inf := fun x y z h1 h2 => show x.1 ≤ y.1 ⊓ z.1 from le_inf h1 h2538539/-- The principal ideal is an ordered additive monoid. -/540instance instIsOrderedAddMonoidPrincipal (a : X) :541 @IsOrderedAddMonoid ↥(principalSubmodule a)542 inferInstance (instLatticePrincipal a).toPartialOrder.toPreorder where543 add_le_add_left := fun x y (h : x.1 ≤ y.1) z =>544 show x.1 + z.1 ≤ y.1 + z.1 from add_le_add_left h _545546/-- In an Archimedean vector lattice, the principal ideal `I_a` with the gauge547norm is a normed additive commutative group. -/548@[reducible]549noncomputable def principalNormedAddCommGroup [IsVLArchimedean X]550 (a : X) :551 NormedAddCommGroup ↥(principalSubmodule a) :=552 NormedAddCommGroup.ofCore (𝕜 := ℝ) {553 toCore := {554 norm_nonneg := fun x => gaugeNorm_nonneg a x.1555 norm_smul := fun r x => gaugeNorm_smul a r x.1556 norm_triangle := fun x y => gaugeNorm_add_le a x.2 y.2557 }558 norm_eq_zero_iff := fun x => (gaugeNorm_eq_zero_iff a x.2).trans559 ⟨fun h => Subtype.ext h, fun h => congr_arg Subtype.val h⟩560 }561562/-- In an Archimedean vector lattice, the principal ideal `I_a` with the gauge563norm admits a `VectorLattice` structure. -/564@[reducible]565noncomputable def principalVectorLattice (a : X) :566 @VectorLattice ↥(principalSubmodule a) inferInstance567 (instLatticePrincipal a)568 (instIsOrderedAddMonoidPrincipal a) where569 toModule := (principalSubmodule a).module570 smul_le_smul_of_nonneg_left := by571 intro c hc x y hxy572 change c • x.1 ≤ c • y.1573 exact smul_le_smul_of_nonneg_left hxy hc574575/-- In an Archimedean vector lattice, the principal ideal `I_a` equipped with576the gauge norm is a normed vector lattice. -/577@[reducible]578noncomputable def principalNormedVectorLattice [IsVLArchimedean X]579 (a : X) :580 @NormedVectorLattice ↥(principalSubmodule a)581 (principalNormedAddCommGroup a)582 (instLatticePrincipal a)583 (instIsOrderedAddMonoidPrincipal a) := by584 letI : NormedAddCommGroup ↥(principalSubmodule a) := principalNormedAddCommGroup a585 letI : Lattice ↥(principalSubmodule a) := instLatticePrincipal a586 letI : IsOrderedAddMonoid ↥(principalSubmodule a) := instIsOrderedAddMonoidPrincipal a587 letI : VectorLattice ↥(principalSubmodule a) := principalVectorLattice a588 let solidNorm : HasSolidNorm ↥(principalSubmodule a) := {589 solid := by590 intro x y h591 change gaugeNorm a x.1 ≤ gaugeNorm a y.1592 exact gaugeNorm_mono_abs a y.2 h593 }594 let normSmul : NormSMulClass ℝ ↥(principalSubmodule a) := {595 norm_smul := by596 intro r x597 change gaugeNorm a (r • x.1) = ‖r‖ * gaugeNorm a x.1598 rw [gaugeNorm_smul a r x.1, Real.norm_eq_abs]599 }600 exact @NormedVectorLattice.mk ↥(principalSubmodule a)601 (principalNormedAddCommGroup a)602 (instLatticePrincipal a)603 (instIsOrderedAddMonoidPrincipal a)604 (principalVectorLattice a)605 solidNorm606 normSmul607608/-! ### Sum of ideals -/609610/-- A non-negative element dominated by a sum `u₁ + u₂` of positive elements of611`J₁` and `J₂` can be split accordingly, so it lies in `J₁ + J₂`. -/612private theorem sum_pos_mem (J₁ J₂ : OrderIdeal X) {v u₁ u₂ : X}613 (hu₁ : u₁ ∈ J₁) (hu₂ : u₂ ∈ J₂) (hu₁0 : 0 ≤ u₁) (hu₂0 : 0 ≤ u₂)614 (hv0 : 0 ≤ v) (hvle : v ≤ u₁ + u₂) :615 v ∈ J₁.toSubmodule + J₂.toSubmodule := by616 have hv₁ : v ⊓ u₁ ∈ J₁ := J₁.solid hu₁ (le_inf hv0 hu₁0) inf_le_right617 have heq : v - v ⊓ u₁ = (v - u₁)⁺ := by618 rw [inf_eq_sub_posPart_sub]; abel619 have hv₂ : v - v ⊓ u₁ ∈ J₂ := by620 rw [heq]621 exact J₂.solid hu₂ (posPart_nonneg _)622 (sup_le (sub_le_iff_le_add'.mpr hvle) hu₂0)623 refine Submodule.mem_sup.mpr ⟨v ⊓ u₁, hv₁, v - v ⊓ u₁, hv₂, ?_⟩624 abel625626/-- The sum of two order ideals (as submodules) is again an order ideal. -/627def sum (J₁ J₂ : OrderIdeal X) : OrderIdeal X :=628 ofSolid (J₁.toSubmodule + J₂.toSubmodule) <| by629 intro x y hx hyx630 obtain ⟨x₁, hx₁, x₂, hx₂, rfl⟩ := Submodule.mem_sup.mp hx631 -- `|y| ≤ |x₁| + |x₂|`; split `y⁺` and `y⁻` separately using `sum_pos_mem`.632 have habs : |y| ≤ |x₁| + |x₂| := le_trans hyx (abs_add_le x₁ x₂)633 have h_pos_le : y⁺ ≤ |x₁| + |x₂| :=634 le_trans (sup_le (le_abs_self y) (abs_nonneg y)) habs635 have h_neg_le : y⁻ ≤ |x₁| + |x₂| :=636 le_trans (sup_le (neg_le_abs y) (abs_nonneg y)) habs637 have hpos : y⁺ ∈ J₁.toSubmodule + J₂.toSubmodule :=638 sum_pos_mem J₁ J₂ (J₁.abs_mem hx₁) (J₂.abs_mem hx₂)639 (abs_nonneg _) (abs_nonneg _) (posPart_nonneg _) h_pos_le640 have hneg : y⁻ ∈ J₁.toSubmodule + J₂.toSubmodule :=641 sum_pos_mem J₁ J₂ (J₁.abs_mem hx₁) (J₂.abs_mem hx₂)642 (abs_nonneg _) (abs_nonneg _) (negPart_nonneg _) h_neg_le643 have := (J₁.toSubmodule + J₂.toSubmodule).sub_mem hpos hneg644 rwa [posPart_sub_negPart] at this645646/-- The underlying submodule of `sum J₁ J₂` is `J₁.toSubmodule + J₂.toSubmodule`. -/647@[simp]648theorem sum_toSubmodule (J₁ J₂ : OrderIdeal X) :649 (sum J₁ J₂).toSubmodule = J₁.toSubmodule + J₂.toSubmodule := rfl650651/-- **Positive decomposition** in the sum of two ideals: every non-negative652element of `J₁ + J₂` admits a splitting `y = y₁ + y₂` with `0 ≤ y₁ ∈ J₁` and653`0 ≤ y₂ ∈ J₂`. -/654theorem exists_sum_decomp_nonneg (J₁ J₂ : OrderIdeal X) {y : X}655 (hy : y ∈ J₁.toSubmodule + J₂.toSubmodule) (hy0 : 0 ≤ y) :656 ∃ y₁ y₂ : X, y₁ ∈ J₁ ∧ y₂ ∈ J₂ ∧ y₁ + y₂ = y ∧ 0 ≤ y₁ ∧ 0 ≤ y₂ := by657 obtain ⟨u₁, hu₁, u₂, hu₂, rfl⟩ := Submodule.mem_sup.mp hy658 have hau₁ : |u₁| ∈ J₁ := J₁.abs_mem hu₁659 have hau₂ : |u₂| ∈ J₂ := J₂.abs_mem hu₂660 have hau₁_nn : 0 ≤ |u₁| := abs_nonneg _661 have hau₂_nn : 0 ≤ |u₂| := abs_nonneg _662 have hyle : u₁ + u₂ ≤ |u₁| + |u₂| :=663 add_le_add (le_abs_self u₁) (le_abs_self u₂)664 refine ⟨(u₁ + u₂) ⊓ |u₁|, (u₁ + u₂) - (u₁ + u₂) ⊓ |u₁|,665 J₁.solid hau₁ (le_inf hy0 hau₁_nn) inf_le_right,666 ?_, by abel, le_inf hy0 hau₁_nn, ?_⟩667 · have heq : (u₁ + u₂) - (u₁ + u₂) ⊓ |u₁| = ((u₁ + u₂) - |u₁|)⁺ := by668 rw [inf_eq_sub_posPart_sub]; abel669 rw [heq]670 exact J₂.solid hau₂ (posPart_nonneg _)671 (sup_le (sub_le_iff_le_add'.mpr hyle) hau₂_nn)672 · have heq : (u₁ + u₂) - (u₁ + u₂) ⊓ |u₁| = ((u₁ + u₂) - |u₁|)⁺ := by673 rw [inf_eq_sub_posPart_sub]; abel674 rw [heq]; exact posPart_nonneg _675676/-- **Bounded decomposition** in the sum of two ideals: every element of677`J₁ + J₂` admits a splitting `z = a + b` with `a ∈ J₁`, `b ∈ J₂` and the678lattice estimates `|a| ≤ |z|`, `|b| ≤ |z|`. -/679theorem exists_sum_decomp (J₁ J₂ : OrderIdeal X) {z : X}680 (hz : z ∈ J₁.toSubmodule + J₂.toSubmodule) :681 ∃ a b : X, a ∈ J₁ ∧ b ∈ J₂ ∧ a + b = z ∧ |a| ≤ |z| ∧ |b| ≤ |z| := by682 obtain ⟨u₁, hu₁, u₂, hu₂, rfl⟩ := Submodule.mem_sup.mp hz683 have habs : |u₁ + u₂| ≤ |u₁| + |u₂| := abs_add_le u₁ u₂684 -- Positive part split685 have hxp_le : (u₁ + u₂)⁺ ≤ |u₁| + |u₂| :=686 le_trans (sup_le (le_abs_self _) (abs_nonneg _)) habs687 let ap := (u₁ + u₂)⁺ ⊓ |u₁|688 have hap_nn : 0 ≤ ap := le_inf (posPart_nonneg _) (abs_nonneg _)689 have hap_le_xp : ap ≤ (u₁ + u₂)⁺ := inf_le_left690 have hap_mem : ap ∈ J₁ := J₁.solid (J₁.abs_mem hu₁) hap_nn inf_le_right691 let bp := (u₁ + u₂)⁺ - ap692 have hbp_eq : bp = ((u₁ + u₂)⁺ - |u₁|)⁺ := by693 change (u₁ + u₂)⁺ - (u₁ + u₂)⁺ ⊓ |u₁| = ((u₁ + u₂)⁺ - |u₁|)⁺694 rw [inf_eq_sub_posPart_sub]; abel695 have hbp_nn : 0 ≤ bp := by rw [hbp_eq]; exact posPart_nonneg _696 have hbp_le_xp : bp ≤ (u₁ + u₂)⁺ := sub_le_self _ hap_nn697 have hbp_mem : bp ∈ J₂ := by698 rw [hbp_eq]699 exact J₂.solid (J₂.abs_mem hu₂) (posPart_nonneg _)700 (sup_le (sub_le_iff_le_add'.mpr hxp_le) (abs_nonneg _))701 have hab_p_sum : ap + bp = (u₁ + u₂)⁺ := by702 change ap + ((u₁ + u₂)⁺ - ap) = _703 abel704 -- Negative part split705 have hxn_le : (u₁ + u₂)⁻ ≤ |u₁| + |u₂| :=706 le_trans (sup_le (neg_le_abs _) (abs_nonneg _)) habs707 let an := (u₁ + u₂)⁻ ⊓ |u₁|708 have han_nn : 0 ≤ an := le_inf (negPart_nonneg _) (abs_nonneg _)709 have han_le_xn : an ≤ (u₁ + u₂)⁻ := inf_le_left710 have han_mem : an ∈ J₁ := J₁.solid (J₁.abs_mem hu₁) han_nn inf_le_right711 let bn := (u₁ + u₂)⁻ - an712 have hbn_eq : bn = ((u₁ + u₂)⁻ - |u₁|)⁺ := by713 change (u₁ + u₂)⁻ - (u₁ + u₂)⁻ ⊓ |u₁| = ((u₁ + u₂)⁻ - |u₁|)⁺714 rw [inf_eq_sub_posPart_sub]; abel715 have hbn_nn : 0 ≤ bn := by rw [hbn_eq]; exact posPart_nonneg _716 have hbn_le_xn : bn ≤ (u₁ + u₂)⁻ := sub_le_self _ han_nn717 have hbn_mem : bn ∈ J₂ := by718 rw [hbn_eq]719 exact J₂.solid (J₂.abs_mem hu₂) (posPart_nonneg _)720 (sup_le (sub_le_iff_le_add'.mpr hxn_le) (abs_nonneg _))721 have hab_n_sum : an + bn = (u₁ + u₂)⁻ := by722 change an + ((u₁ + u₂)⁻ - an) = _723 abel724 -- Assemble725 refine ⟨ap - an, bp - bn,726 J₁.toSubmodule.sub_mem hap_mem han_mem,727 J₂.toSubmodule.sub_mem hbp_mem hbn_mem, ?_, ?_, ?_⟩728 · calc ap - an + (bp - bn)729 = (ap + bp) - (an + bn) := by abel730 _ = (u₁ + u₂)⁺ - (u₁ + u₂)⁻ := by rw [hab_p_sum, hab_n_sum]731 _ = u₁ + u₂ := posPart_sub_negPart _732 · calc |ap - an|733 = |ap + (-an)| := by rw [sub_eq_add_neg]734 _ ≤ |ap| + |(-an)| := abs_add_le _ _735 _ = ap + an := by rw [abs_of_nonneg hap_nn, abs_neg, abs_of_nonneg han_nn]736 _ ≤ (u₁ + u₂)⁺ + (u₁ + u₂)⁻ := add_le_add hap_le_xp han_le_xn737 _ = |u₁ + u₂| := posPart_add_negPart _738 · calc |bp - bn|739 = |bp + (-bn)| := by rw [sub_eq_add_neg]740 _ ≤ |bp| + |(-bn)| := abs_add_le _ _741 _ = bp + bn := by rw [abs_of_nonneg hbp_nn, abs_neg, abs_of_nonneg hbn_nn]742 _ ≤ (u₁ + u₂)⁺ + (u₁ + u₂)⁻ := add_le_add hbp_le_xp hbn_le_xn743 _ = |u₁ + u₂| := posPart_add_negPart _744745/-! ### Complete lattice structure -/746747/-- The whole space `X` is an order ideal. -/748instance : Top (OrderIdeal X) where749 top :=750 { toSubmodule := ⊤751 sup_mem' := fun _ _ => Submodule.mem_top752 solid' := fun _ _ _ => Submodule.mem_top }753754@[simp] theorem mem_top {x : X} : x ∈ (⊤ : OrderIdeal X) := Submodule.mem_top755756/-- The trivial ideal `{0}` is an order ideal. -/757instance : Bot (OrderIdeal X) where758 bot :=759 { toSubmodule := ⊥760 sup_mem' := fun {x y} hx hy => by761 have hx' : x = 0 := (Submodule.mem_bot ℝ).mp hx762 have hy' : y = 0 := (Submodule.mem_bot ℝ).mp hy763 rw [hx', hy', sup_idem]; exact Submodule.zero_mem _764 solid' := fun {x y} hx hy0 hyx => by765 have hx' : x = 0 := (Submodule.mem_bot ℝ).mp hx766 rw [hx'] at hyx767 exact (Submodule.mem_bot ℝ).mpr (le_antisymm hyx hy0) }768769@[simp] theorem mem_bot {x : X} : x ∈ (⊥ : OrderIdeal X) ↔ x = 0 :=770 Submodule.mem_bot ℝ771772/-- Order ideals of `X`, ordered by inclusion, form a **complete lattice**.773Binary joins are given by the (Minkowski) sum `sum`, binary meets and arbitrary774infima are given by intersection, the bottom element is the trivial ideal775`{0}`, and the top element is the whole space. -/776instance : CompleteLattice (OrderIdeal X) where777 __ := (inferInstance : PartialOrder (OrderIdeal X))778 sup := sum779 inf := OrderIdeal.inf780 top := ⊤781 bot := ⊥782 sInf := sInf783 sSup S := sInf {K : OrderIdeal X | ∀ I ∈ S, I ≤ K}784 le_top := fun _ _ _ => Submodule.mem_top785 bot_le := fun J x hx => by786 have hx' : x ∈ (⊥ : Submodule ℝ X) := hx787 have : x = 0 := (Submodule.mem_bot ℝ).mp hx'788 exact this ▸ J.toSubmodule.zero_mem789 le_sup_left := fun J₁ J₂ x hx =>790 Submodule.mem_sup.mpr ⟨x, hx, 0, J₂.toSubmodule.zero_mem, add_zero x⟩791 le_sup_right := fun J₁ J₂ x hx =>792 Submodule.mem_sup.mpr ⟨0, J₁.toSubmodule.zero_mem, x, hx, zero_add x⟩793 sup_le := fun J₁ J₂ K hJ₁ hJ₂ x hx => by794 obtain ⟨x₁, hx₁, x₂, hx₂, rfl⟩ := Submodule.mem_sup.mp hx795 exact K.toSubmodule.add_mem (hJ₁ hx₁) (hJ₂ hx₂)796 inf_le_left := fun _ _ _ hx => hx.1797 inf_le_right := fun _ _ _ hx => hx.2798 le_inf := fun _ _ _ h₁ h₂ _ hx => ⟨h₁ hx, h₂ hx⟩799 isLUB_sSup := fun S => by800 refine ⟨?_, ?_⟩801 · intro J hJ x hx802 rw [mem_sInf]803 intro K hK804 exact hK J hJ hx805 · intro J hJ x hx806 rw [mem_sInf] at hx807 exact hx J hJ808 isGLB_sInf := fun S => by809 refine ⟨?_, ?_⟩810 · intro J hJ x hx811 rw [mem_sInf] at hx812 exact hx J hJ813 · intro J hJ x hx814 rw [mem_sInf]815 intro K hK816 exact hJ hK hx817818@[simp] theorem sup_toSubmodule (J₁ J₂ : OrderIdeal X) :819 (J₁ ⊔ J₂).toSubmodule = J₁.toSubmodule + J₂.toSubmodule := rfl820821@[simp] theorem inf_toSubmodule (J₁ J₂ : OrderIdeal X) :822 (J₁ ⊓ J₂).toSubmodule = J₁.toSubmodule ⊓ J₂.toSubmodule := rfl823824/-! ### Strong order units and the principal ideal -/825826/-- An element is a strong order unit precisely when it is non-negative and the827principal ideal it generates is the whole space. -/828theorem strongOrderUnit_iff_principal_eq_top {e : X} :829 StrongOrderUnit e ↔ 0 ≤ e ∧ principal e = ⊤ := by830 refine ⟨fun ⟨he, hdom⟩ => ⟨he, ?_⟩, fun ⟨he, htop⟩ => ⟨he, fun x => ?_⟩⟩831 · refine SetLike.ext fun x => iff_of_true ?_ mem_top832 obtain ⟨c, hc, hxc⟩ := hdom x833 exact ⟨c, hc, by rwa [abs_of_nonneg he]⟩834 · have hx : x ∈ principal e := htop ▸ mem_top835 obtain ⟨c, hc, hxc⟩ := hx836 exact ⟨c, hc, by rwa [abs_of_nonneg he] at hxc⟩837838/-! ### Existence of proper non-trivial ideals -/839840/-- Two non-negative lattice-disjoint elements cannot sit in a common principal841ideal: if `0 ≤ p, q` with `p ⊓ q = 0` and `q ∈ principal p`, then `q = 0`. -/842private lemma eq_zero_of_mem_principal_disjoint {p q : X} (hp : 0 ≤ p)843 (hq : 0 ≤ q) (hpq : p ⊓ q = 0) (hq_in : q ∈ principal p) : q = 0 := by844 obtain ⟨c, hc, hle⟩ := hq_in845 rw [abs_of_nonneg hq, abs_of_nonneg hp] at hle846 rcases le_or_gt 1 c with h1 | h1847 · have hq_le_cq : q ≤ c • q := by848 calc q = (1 : ℝ) • q := (one_smul ℝ q).symm849 _ ≤ c • q := smul_le_smul_of_nonneg_right h1 hq850 have hboth : q ≤ c • p ⊓ c • q := le_inf hle hq_le_cq851 rw [← nonneg_smul_inf p q c (le_trans zero_le_one h1), hpq, smul_zero] at hboth852 exact le_antisymm hboth hq853 · have hcp_le_p : c • p ≤ p := by854 calc c • p ≤ (1 : ℝ) • p := smul_le_smul_of_nonneg_right h1.le hp855 _ = p := one_smul ℝ p856 have hq_le_p : q ≤ p := le_trans hle hcp_le_p857 have : p ⊓ q = q := inf_eq_right.mpr hq_le_p858 rwa [this] at hpq859860/-- If the real dimension of `X` is strictly greater than one, then `X` admits861an order ideal that is **neither trivial nor the whole space**. -/862theorem exists_proper_nontrivial [IsVLArchimedean X] (h : 1 < Module.rank ℝ X) :863 ∃ J : OrderIdeal X, J ≠ ⊥ ∧ J ≠ ⊤ := by864 obtain ⟨u, v, hu, hv, huv⟩ := exists_pair_ne_zero_isVLDisjoint h865 have habs_u_nn : 0 ≤ |u| := abs_nonneg u866 have habs_v_nn : 0 ≤ |v| := abs_nonneg v867 have habs_u_nz : |u| ≠ 0 := fun h => hu ((abs_eq_zero_iff_zero u).mp h)868 have habs_v_nz : |v| ≠ 0 := fun h => hv ((abs_eq_zero_iff_zero v).mp h)869 refine ⟨principal (|u|), ?_, ?_⟩870 · intro heq871 have : (|u| : X) ∈ (⊥ : OrderIdeal X) := heq ▸ self_mem_principal |u|872 exact habs_u_nz (mem_bot.mp this)873 · intro heq874 have hv_mem : (|v| : X) ∈ principal (|u|) := heq ▸ mem_top875 exact habs_v_nz876 (eq_zero_of_mem_principal_disjoint habs_u_nn habs_v_nn huv hv_mem)877878/-! ### Closure of an ideal in a normed vector lattice -/879880section Closure881882variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]883 [NormedVectorLattice X]884885/-- The topological closure of the underlying submodule of an order ideal is886itself solid: if `x` lies in the closure and `|y| ≤ |x|`, then `y` lies in the887closure. -/888theorem topologicalClosure_solid (J : OrderIdeal X) :889 ∀ x y : X, x ∈ J.toSubmodule.topologicalClosure → |y| ≤ |x| →890 y ∈ J.toSubmodule.topologicalClosure := by891 intro x y hx hy_abs892 have hx' : x ∈ closure (J.toSubmodule : Set X) := by893 rwa [← Submodule.topologicalClosure_coe]894 obtain ⟨xn, hxn_mem, hxn_lim⟩ := mem_closure_iff_seq_limit.mp hx'895 -- Truncated sequence yₙ = (y ⊔ -|xₙ|) ⊓ |xₙ|, which lies in J and converges to y.896 set yn : ℕ → X := fun n => (y ⊔ (-|xn n|)) ⊓ |xn n| with hyn_def897 have habs_nn : ∀ n, (0 : X) ≤ |xn n| := fun _ => abs_nonneg _898 have hyn_mem : ∀ n, yn n ∈ J.toSubmodule := by899 intro n900 have habs_mem : |xn n| ∈ J := J.abs_mem (hxn_mem n)901 have h_le : yn n ≤ |xn n| := inf_le_right902 have h_neg_le : -|xn n| ≤ |xn n| :=903 le_trans (neg_nonpos_of_nonneg (habs_nn n)) (habs_nn n)904 have h_ge : -|xn n| ≤ yn n := le_inf le_sup_right h_neg_le905 have h_abs_yn : |yn n| ≤ |xn n| := by906 rw [abs_le']; exact ⟨h_le, by rwa [neg_le]⟩907 have : |yn n| ∈ J := J.solid habs_mem (abs_nonneg _) h_abs_yn908 exact J.mem_of_abs_mem this909 -- Continuity of `|·|`, `⊔`, `⊓` makes `yn → y`.910 have hcont_abs : Continuous (|·| : X → X) :=911 NormedVectorLattice.lipschitzWith_abs.continuous912 have habs_tendsto : Filter.Tendsto (fun n => |xn n|) Filter.atTop (nhds |x|) :=913 (hcont_abs.tendsto _).comp hxn_lim914 have hneg_tendsto : Filter.Tendsto (fun n => -|xn n|) Filter.atTop (nhds (-|x|)) :=915 habs_tendsto.neg916 have hsup_tendsto :917 Filter.Tendsto (fun n => y ⊔ (-|xn n|)) Filter.atTop (nhds (y ⊔ (-|x|))) :=918 (NormedVectorLattice.continuous_sup.tendsto _).comp919 (tendsto_const_nhds.prodMk_nhds hneg_tendsto)920 have hyn_tendsto :921 Filter.Tendsto yn Filter.atTop (nhds ((y ⊔ (-|x|)) ⊓ |x|)) :=922 (NormedVectorLattice.continuous_inf.tendsto _).comp923 (hsup_tendsto.prodMk_nhds habs_tendsto)924 have h_le_abs : y ≤ |x| := le_trans (le_abs_self y) hy_abs925 have h_neg_le : -|x| ≤ y := by rw [neg_le]; exact le_trans (neg_le_abs y) hy_abs926 have hy_eq : (y ⊔ (-|x|)) ⊓ |x| = y := by927 rw [sup_eq_left.mpr h_neg_le, inf_eq_left.mpr h_le_abs]928 rw [hy_eq] at hyn_tendsto929 have hy_in_closure : y ∈ closure (J.toSubmodule : Set X) :=930 mem_closure_of_tendsto hyn_tendsto (Filter.Eventually.of_forall hyn_mem)931 rwa [← Submodule.topologicalClosure_coe] at hy_in_closure932933/-- The **norm closure** of an order ideal `J` in a normed vector lattice is934again an order ideal, whose underlying submodule is the topological closure of935`J.toSubmodule`. -/936def topologicalClosure (J : OrderIdeal X) : OrderIdeal X :=937 ofSolid J.toSubmodule.topologicalClosure (topologicalClosure_solid J)938939@[simp]940theorem topologicalClosure_toSubmodule (J : OrderIdeal X) :941 (topologicalClosure J).toSubmodule = J.toSubmodule.topologicalClosure := rfl942943end Closure944945end OrderIdeal946947/-- A **closed order ideal** of a Banach lattice is an order ideal whose948underlying set is closed in the norm topology. -/949structure ClosedOrderIdeal (X : Type*) [NormedAddCommGroup X]950 [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X]951 extends OrderIdeal X where952 isClosed' : IsClosed (toOrderIdeal : Set X)953954namespace ClosedOrderIdeal955956variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]957 [BanachLattice X]958959instance : SetLike (ClosedOrderIdeal X) X where960 coe J := J.toOrderIdeal961 coe_injective p q h := by962 cases p; cases q; congr963 exact SetLike.coe_injective h964965/-- A closed order ideal is closed as a subset of `X`. -/966theorem isClosed (J : ClosedOrderIdeal X) : IsClosed (J : Set X) :=967 J.isClosed'968969/-- Closed order ideals form a partial order under inclusion. -/970instance : PartialOrder (ClosedOrderIdeal X) :=971 .ofSetLike (ClosedOrderIdeal X) X972973/-- The intersection of two closed order ideals is a closed order ideal. -/974def inf (J₁ J₂ : ClosedOrderIdeal X) : ClosedOrderIdeal X where975 toOrderIdeal := J₁.toOrderIdeal ⊓ J₂.toOrderIdeal976 isClosed' := J₁.isClosed.inter J₂.isClosed977978/-- **Norm-bounded decomposition** in the sum of two ideals of a normed vector979lattice: every element of `J₁ + J₂` splits as `z = a + b` with `a ∈ J₁`,980`b ∈ J₂` and `‖a‖ ≤ ‖z‖`, `‖b‖ ≤ ‖z‖`. -/981private theorem exists_sum_decomp_norm (J₁ J₂ : OrderIdeal X) {z : X}982 (hz : z ∈ J₁.toSubmodule + J₂.toSubmodule) :983 ∃ a b : X, a ∈ J₁ ∧ b ∈ J₂ ∧ a + b = z ∧ ‖a‖ ≤ ‖z‖ ∧ ‖b‖ ≤ ‖z‖ := by984 obtain ⟨a, b, ha, hb, hsum, habs_a, habs_b⟩ := OrderIdeal.exists_sum_decomp J₁ J₂ hz985 refine ⟨a, b, ha, hb, hsum, ?_, ?_⟩986 · rw [← norm_abs_eq_norm z]; exact norm_le_norm_of_abs_le_abs (by rwa [abs_abs])987 · rw [← norm_abs_eq_norm z]; exact norm_le_norm_of_abs_le_abs (by rwa [abs_abs])988989/-- The sum of two closed order ideals in a Banach lattice is again closed. -/990private theorem isClosed_sum {J₁ J₂ : OrderIdeal X}991 (h₁ : IsClosed (J₁ : Set X)) (h₂ : IsClosed (J₂ : Set X)) :992 IsClosed ((OrderIdeal.sum J₁ J₂ : OrderIdeal X) : Set X) := by993 rw [← isSeqClosed_iff_isClosed]994 intro z_seq z hz_mem hz_lim995 -- Extract a subsequence whose consecutive distances are summable.996 have hCauchy : CauchySeq z_seq := hz_lim.cauchySeq997 obtain ⟨φ, hφ_mono, hφ_sum⟩ :=998 Metric.exists_subseq_summable_dist_of_cauchySeq z_seq hCauchy999 -- The subsequence still converges to z.1000 have hsub_lim : Filter.Tendsto (z_seq ∘ φ) Filter.atTop (nhds z) :=1001 hz_lim.comp hφ_mono.tendsto_atTop1002 -- Differences along the subsequence.1003 set w : ℕ → X := fun k => z_seq (φ (k + 1)) - z_seq (φ k) with hw_def1004 have hw_norm : ∀ k, ‖w k‖ = dist (z_seq (φ (k + 1))) (z_seq (φ k)) := by1005 intro k; rw [hw_def, dist_eq_norm]1006 have hw_summable : Summable fun k => ‖w k‖ := by1007 simpa [hw_norm] using hφ_sum1008 have hw_mem : ∀ k, w k ∈ J₁.toSubmodule + J₂.toSubmodule := fun k =>1009 (J₁.toSubmodule + J₂.toSubmodule).sub_mem (hz_mem _) (hz_mem _)1010 -- Decompose each difference with norm bounds.1011 choose a b ha hb hab ha_norm hb_norm using1012 fun k => exists_sum_decomp_norm J₁ J₂ (hw_mem k)1013 have ha_summable : Summable fun k => ‖a k‖ :=1014 hw_summable.of_nonneg_of_le (fun _ => norm_nonneg _) ha_norm1015 have hb_summable : Summable fun k => ‖b k‖ :=1016 hw_summable.of_nonneg_of_le (fun _ => norm_nonneg _) hb_norm1017 have ha_sum : Summable a := ha_summable.of_norm1018 have hb_sum : Summable b := hb_summable.of_norm1019 obtain ⟨A, hA_hasSum⟩ := ha_sum1020 obtain ⟨B, hB_hasSum⟩ := hb_sum1021 -- The partial sums of `a` live in the closed ideal `J₁`, hence so does `A`.1022 have hA_mem : A ∈ J₁ :=1023 h₁.mem_of_tendsto hA_hasSum1024 (Filter.Eventually.of_forall fun s =>1025 J₁.toSubmodule.sum_mem (fun k _ => ha k))1026 have hB_mem : B ∈ J₂ :=1027 h₂.mem_of_tendsto hB_hasSum1028 (Filter.Eventually.of_forall fun s =>1029 J₂.toSubmodule.sum_mem (fun k _ => hb k))1030 -- `w k = a k + b k`, so `HasSum w (A + B)`.1031 have hw_hasSum : HasSum w (A + B) := by1032 have : HasSum (fun k => a k + b k) (A + B) := hA_hasSum.add hB_hasSum1033 convert this using 11034 funext k; exact (hab k).symm1035 -- Telescoping: partial sums of `w` tend to `z - z_seq (φ 0)`.1036 have htelescope : Filter.Tendsto1037 (fun n : ℕ => ∑ k ∈ Finset.range n, w k) Filter.atTop1038 (nhds (z - z_seq (φ 0))) := by1039 have hsum_eq : ∀ n, (∑ k ∈ Finset.range n, w k)1040 = z_seq (φ n) - z_seq (φ 0) := by1041 intro n1042 simpa [hw_def] using1043 Finset.sum_range_sub (fun k => z_seq (φ k)) n1044 simp only [hsum_eq]1045 exact hsub_lim.sub_const _1046 -- Identify the two limits of the partial sums.1047 have hAB_eq : A + B = z - z_seq (φ 0) :=1048 tendsto_nhds_unique hw_hasSum.tendsto_sum_nat htelescope1049 have hz_eq : z = z_seq (φ 0) + (A + B) := by rw [hAB_eq]; abel1050 change z ∈ (J₁.toSubmodule + J₂.toSubmodule : Submodule ℝ X)1051 rw [hz_eq]1052 exact (J₁.toSubmodule + J₂.toSubmodule).add_mem1053 (hz_mem (φ 0))1054 (Submodule.mem_sup.mpr ⟨A, hA_mem, B, hB_mem, rfl⟩)10551056/-- The sum of two closed order ideals of a Banach lattice is again a closed1057order ideal. -/1058def sup (J₁ J₂ : ClosedOrderIdeal X) : ClosedOrderIdeal X where1059 toOrderIdeal := OrderIdeal.sum J₁.toOrderIdeal J₂.toOrderIdeal1060 isClosed' := isClosed_sum J₁.isClosed J₂.isClosed10611062/-- The arbitrary intersection of a family of closed order ideals is a closed1063order ideal. -/1064def sInf (S : Set (ClosedOrderIdeal X)) : ClosedOrderIdeal X where1065 toOrderIdeal := InfSet.sInf ((·.toOrderIdeal) '' S)1066 isClosed' := by1067 have h : ((InfSet.sInf ((·.toOrderIdeal) '' S) : OrderIdeal X) : Set X) =1068 ⋂ J ∈ S, (J : Set X) := by1069 ext x1070 rw [Set.mem_iInter₂]1071 exact OrderIdeal.mem_sInf.trans1072 ⟨fun h J hJ => h _ ⟨J, hJ, rfl⟩, by rintro h _ ⟨J, hJ, rfl⟩; exact h J hJ⟩1073 rw [show ((InfSet.sInf ((·.toOrderIdeal) '' S) : OrderIdeal X) : Set X) =1074 ⋂ J ∈ S, (J : Set X) from h]1075 exact isClosed_biInter fun J _ => J.isClosed10761077/-- Closed order ideals of a Banach lattice form a **lattice** under inclusion,1078with binary meets given by intersection and binary joins by the sum. -/1079instance : Lattice (ClosedOrderIdeal X) where1080 sup := sup1081 inf := inf1082 le_sup_left := fun J₁ J₂ x hx => by1083 change x ∈ OrderIdeal.sum J₁.toOrderIdeal J₂.toOrderIdeal1084 exact Submodule.mem_sup.mpr ⟨x, hx, 0, J₂.toSubmodule.zero_mem, add_zero x⟩1085 le_sup_right := fun J₁ J₂ x hx => by1086 change x ∈ OrderIdeal.sum J₁.toOrderIdeal J₂.toOrderIdeal1087 exact Submodule.mem_sup.mpr ⟨0, J₁.toSubmodule.zero_mem, x, hx, zero_add x⟩1088 sup_le := fun J₁ J₂ K hJ₁ hJ₂ x hx => by1089 obtain ⟨x₁, hx₁, x₂, hx₂, rfl⟩ := Submodule.mem_sup.mp hx1090 exact K.toSubmodule.add_mem (hJ₁ hx₁) (hJ₂ hx₂)1091 inf_le_left := fun _ _ _ hx => hx.11092 inf_le_right := fun _ _ _ hx => hx.21093 le_inf := fun _ _ _ h₁ h₂ _ hx => ⟨h₁ hx, h₂ hx⟩10941095/-- Closed order ideals of a Banach lattice admit **arbitrary intersections**:1096they form a complete semilattice for the `⊓` operation. -/1097instance : InfSet (ClosedOrderIdeal X) where1098 sInf := sInf10991100/-- Membership in an arbitrary intersection of closed order ideals. -/1101@[simp] theorem mem_sInf {S : Set (ClosedOrderIdeal X)} {x : X} :1102 x ∈ (InfSet.sInf S : ClosedOrderIdeal X) ↔ ∀ J ∈ S, x ∈ J := by1103 change x ∈ (InfSet.sInf ((·.toOrderIdeal) '' S) : OrderIdeal X) ↔ _1104 rw [OrderIdeal.mem_sInf]1105 refine ⟨fun h J hJ => h _ ⟨J, hJ, rfl⟩, ?_⟩1106 rintro h _ ⟨J, hJ, rfl⟩; exact h J hJ11071108/-- The underlying submodule of a binary meet is the intersection of the1109underlying submodules. -/1110@[simp] theorem inf_toSubmodule (J₁ J₂ : ClosedOrderIdeal X) :1111 (J₁ ⊓ J₂).toSubmodule = J₁.toSubmodule ⊓ J₂.toSubmodule := rfl11121113/-- The underlying submodule of a binary join is the sum of the underlying1114submodules. -/1115@[simp] theorem sup_toSubmodule (J₁ J₂ : ClosedOrderIdeal X) :1116 (J₁ ⊔ J₂).toSubmodule = J₁.toSubmodule + J₂.toSubmodule := rfl11171118end ClosedOrderIdeal1119