BanLat/Basic.lean
All source files · Download exact source
SHA-256: 30d3f545bce051b3621a881ae7c374d9d98b37bb14d20ed2ae339668f49dbfed
1/-2Authors: David Muñoz-Lahoz3-/45import Mathlib.Basic.Real.Basic6import Mathlib.Algebra.Order.Module.Defs7import Mathlib.Algebra.Order.Monoid.Defs8import Mathlib.Algebra.Order.Archimedean.Real.Basic9import Mathlib.LinearAlgebra.Dimension.DivisionRing10import Mathlib.Tactic.Abel11import Mathlib.Tactic.FinCases12import Mathlib.Tactic.FieldSimp13import Mathlib.Tactic.GCongr14import Mathlib.Tactic.Linarith15import Mathlib.Tactic.Positivity16import Mathlib.Tactic.Ring1718/-!19# Lattice-ordered groups and vector lattices2021This file develops the basic order-theoretic algebra of lattice-ordered groups and vector22lattices. The first part works in the general setting of an additive commutative group with a23compatible lattice order (`IsOrderedAddMonoid`): it establishes properties of `x⁺`, `x⁻`,24and `|x|`, together with order-theoretic suprema and infima lemmas. The second part adds a25real scalar multiplication (`VectorLattice`) and proves that positive scalars distribute over26`⊔` and `⊓`, culminating in `abs_smul'`. The Archimedean case is treated at the end.27-/2829/-- A real vector lattice is a real module whose scalar multiplication is monotone for30non-negative scalars and is compatible with the lattice-ordered additive structure. -/31class VectorLattice (X : Type*) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] extends32 Module ℝ X,33 PosSMulMono ℝ X3435/-- The real numbers form a vector lattice over themselves. -/36noncomputable instance : VectorLattice ℝ where3738section LatticeOrderedGroup3940variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]4142variable (x : X)4344/-- An element of a lattice-ordered group is zero iff its absolute value is zero.45Extends `Mathlib.Algebra.Order.Module.Basic.abs_eq_zero` to the non-total-order setting. -/46theorem abs_eq_zero_iff_zero : |x| = 0 ↔ x = 0 := by47 constructor48 · intro h49 rw [← negPart_add_posPart, add_eq_zero_iff_eq_neg] at h50 have h1 : x⁺ = 0 := by51 apply le_antisymm52 · rw [← neg_zero]53 apply le_neg_of_le_neg54 rw [← h]55 exact negPart_nonneg x56 · exact posPart_nonneg x57 have h2 : x⁻ = 0 := by58 apply le_antisymm59 · rw [h]60 apply neg_le_of_neg_le61 rw [neg_zero]62 exact posPart_nonneg x63 · exact negPart_nonneg x64 rw [← posPart_sub_negPart x]65 rw [h1, h2]66 simp67 · intro h68 simp [h]6970/-- If `x = u - v` with `u ⊓ v = 0`, then `u` is the positive part of `x`. -/71theorem uniqueness_posPart {u v : X} (hdif : x = u - v) (udisv : u ⊓ v = 0) :72 u = x⁺ := by73 symm74 calc75 x⁺ = x ⊔ 0 := by rfl76 _ = (u - v) ⊔ 0 := by rw [hdif]77 _ = u ⊔ v + (-v) := by rw [add_comm, add_sup]; simp [sub_eq_add_neg, add_comm]78 _ = u + v + (-v) := by rw [← inf_add_sup u v, udisv, zero_add]79 _ = u := by simp8081/-- `x ⊔ y = x + (y - x)⁺`. -/82theorem sup_eq_add_posPart (y : X) : x ⊔ y = x + (y - x)⁺ := by83 rw [posPart_def, add_sup, add_sub_cancel, add_zero, sup_comm]8485/-- `x ⊓ y = x - (x - y)⁺`. -/86theorem inf_eq_sub_posPart (y : X) : x ⊓ y = x - (x - y)⁺ := by87 rw [posPart_def, sub_eq_add_neg, neg_sup, neg_sub, neg_zero, add_inf, add_zero, inf_comm]88 congr 1; abel8990/-- `x - x ⊓ y = (x - y)⁺`. -/91theorem sub_inf_eq_posPart (y : X) : x - x ⊓ y = (x - y)⁺ := by92 rw [inf_eq_sub_posPart, sub_sub_cancel]9394/-- The positive part is subadditive: `(x + y)⁺ ≤ x⁺ + y⁺`. -/95theorem posPart_add_le (y : X) : (x + y)⁺ ≤ x⁺ + y⁺ :=96 sup_le (add_le_add (le_posPart x) (le_posPart y))97 (add_nonneg (posPart_nonneg x) (posPart_nonneg y))9899/-- The positive part is bounded by the modulus. -/100theorem posPart_le_abs : x⁺ ≤ |x| := by101 rw [posPart_def]102 exact sup_le (le_abs_self x) (abs_nonneg x)103104/-- The negative part is bounded by the modulus. -/105theorem negPart_le_abs : x⁻ ≤ |x| := by106 rw [negPart_def]107 exact sup_le (neg_le_abs x) (abs_nonneg x)108109/-- For non-negative `x`, `a`, `b`: `x ⊓ (a + b) ≤ x ⊓ a + x ⊓ b`. -/110theorem inf_le_inf_add_inf_of_nonneg (a b : X) (hx : 0 ≤ x) (ha : 0 ≤ a) (hb : 0 ≤ b) :111 x ⊓ (a + b) ≤ x ⊓ a + x ⊓ b := by112 set c := x ⊓ (a + b) with hc_def113 have hcx : c ≤ x := inf_le_left114 have hcab : c ≤ a + b := inf_le_right115 have hca_nn : 0 ≤ c ⊓ a := le_inf (le_inf hx (add_nonneg ha hb)) ha116 have h1 : c - c ⊓ a = (c - a)⁺ := sub_inf_eq_posPart c a117 have h2 : (c - a)⁺ ≤ b := by118 rw [← posPart_of_nonneg hb]119 exact posPart_mono (sub_le_iff_le_add.mpr (by rwa [add_comm]))120 have h3 : c - c ⊓ a ≤ x := by121 have := sub_le_self c hca_nn122 exact this.trans hcx123 have h4 : c - c ⊓ a ≤ x ⊓ b := le_inf h3 (h1 ▸ h2)124 have h5 : c ⊓ a ≤ x ⊓ a := inf_le_inf_right _ hcx125 have h4' : c ≤ x ⊓ b + c ⊓ a := sub_le_iff_le_add.mp h4126 calc c ≤ x ⊓ b + c ⊓ a := h4'127 _ ≤ x ⊓ b + x ⊓ a := by gcongr128 _ = x ⊓ a + x ⊓ b := add_comm _ _129130/-- Translation preserves suprema: `x + sup A = sup(x + A)`. -/131theorem isLUB_const_add {A : Set X} {a : X} (x : X) (h : IsLUB A a) :132 IsLUB ((fun z => x + z) '' A) (x + a) :=133 (OrderIso.addLeft x).isLUB_image'.mpr h134135/-- Translation preserves infima: `x + inf A = inf(x + A)`. -/136theorem isGLB_const_add {A : Set X} {a : X} (x : X) (h : IsGLB A a) :137 IsGLB ((fun z => x + z) '' A) (x + a) :=138 (OrderIso.addLeft x).isGLB_image'.mpr h139140/-- Meet distributes over arbitrary suprema: `x ⊓ sup A = sup {x ⊓ a : a ∈ A}`. -/141theorem isLUB_inf_const {A : Set X} {a : X} (x : X) (h : IsLUB A a) :142 IsLUB ((fun z => x ⊓ z) '' A) (x ⊓ a) := by143 refine ⟨?_, ?_⟩144 · rintro _ ⟨z, hz, rfl⟩145 exact inf_le_inf_left x (h.1 hz)146 · intro u hu147 have hA : ∀ z ∈ A, z ≤ u + (a - x)⁺ := by148 intro z hz149 have hzu : z - (z - x)⁺ ≤ u := by150 rw [← inf_eq_sub_posPart, inf_comm]; exact hu ⟨z, hz, rfl⟩151 have hmono : (z - x)⁺ ≤ (a - x)⁺ := posPart_mono (sub_le_sub_right (h.1 hz) x)152 have h1 : z ≤ u + (z - x)⁺ := sub_le_iff_le_add.mp hzu153 exact h1.trans (by gcongr)154 have key : a ≤ u + (a - x)⁺ := h.2 hA155 calc x ⊓ a = a ⊓ x := inf_comm _ _156 _ = a - (a - x)⁺ := inf_eq_sub_posPart a x157 _ ≤ u := sub_le_iff_le_add.mpr key158159/-- Join distributes over arbitrary infima: `x ⊔ inf A = inf {x ⊔ a : a ∈ A}`. -/160theorem isGLB_sup_const {A : Set X} {a : X} (x : X) (h : IsGLB A a) :161 IsGLB ((fun z => x ⊔ z) '' A) (x ⊔ a) := by162 refine ⟨?_, ?_⟩163 · rintro _ ⟨z, hz, rfl⟩164 exact sup_le_sup_left (h.1 hz) x165 · intro u hu166 have hA : ∀ z ∈ A, u - (x - a)⁺ ≤ z := by167 intro z hz168 have hzu : u ≤ z + (x - z)⁺ := by169 rw [← sup_eq_add_posPart, sup_comm]; exact hu ⟨z, hz, rfl⟩170 have hmono : (x - z)⁺ ≤ (x - a)⁺ := posPart_mono (sub_le_sub_left (h.1 hz) x)171 exact sub_le_iff_le_add.mpr (hzu.trans (by gcongr))172 have key : u - (x - a)⁺ ≤ a := h.2 hA173 calc u = (u - (x - a)⁺) + (x - a)⁺ := by abel174 _ ≤ a + (x - a)⁺ := by gcongr175 _ = a ⊔ x := (sup_eq_add_posPart a x).symm176 _ = x ⊔ a := sup_comm _ _177178/-- `inf(A + B) = inf A + inf B`. -/179theorem isGLB_add_sets {A B : Set X} {a b : X}180 (hA : IsGLB A a) (hB : IsGLB B b) :181 IsGLB ((fun p : X × X => p.1 + p.2) '' (A ×ˢ B)) (a + b) := by182 refine ⟨?_, ?_⟩183 · rintro _ ⟨⟨p, q⟩, ⟨hp, hq⟩, rfl⟩184 exact add_le_add (hA.1 hp) (hB.1 hq)185 · intro u hu186 have h1 : ∀ p ∈ A, u ≤ p + b := by187 intro p hp188 have hp_lb : u - p ∈ lowerBounds B := fun q hq => by189 have hpq : u ≤ p + q := hu ⟨(p, q), ⟨hp, hq⟩, rfl⟩190 rw [add_comm] at hpq191 exact sub_le_iff_le_add.mpr hpq192 have : u ≤ b + p := sub_le_iff_le_add.mp (hB.2 hp_lb)193 rwa [add_comm] at this194 have h2 : u - b ∈ lowerBounds A := fun p hp =>195 sub_le_iff_le_add.mpr (h1 p hp)196 exact sub_le_iff_le_add.mp (hA.2 h2)197198/-- `inf(A ∨ B) = inf A ∨ inf B`, where `A ∨ B = {p ⊔ q : p ∈ A, q ∈ B}`. -/199theorem isGLB_sup_sets {A B : Set X} {a b : X}200 (hA : IsGLB A a) (hB : IsGLB B b) :201 IsGLB ((fun p : X × X => p.1 ⊔ p.2) '' (A ×ˢ B)) (a ⊔ b) := by202 refine ⟨?_, ?_⟩203 · rintro _ ⟨⟨p, q⟩, ⟨hp, hq⟩, rfl⟩204 exact sup_le_sup (hA.1 hp) (hB.1 hq)205 · intro u hu206 have h1 : ∀ q ∈ B, u ≤ a ⊔ q := by207 intro q hq208 have hlb : u ∈ lowerBounds ((fun z => q ⊔ z) '' A) := by209 rintro _ ⟨p, hp, rfl⟩210 have hpq : u ≤ p ⊔ q := hu ⟨(p, q), ⟨hp, hq⟩, rfl⟩211 rw [sup_comm] at hpq; exact hpq212 have hqa : u ≤ q ⊔ a := (isGLB_sup_const q hA).2 hlb213 rwa [sup_comm] at hqa214 exact (isGLB_sup_const a hB).2 (by rintro _ ⟨q, hq, rfl⟩; exact h1 q hq)215216omit [AddCommGroup X] [IsOrderedAddMonoid X] in217/-- `inf(A ∪ B) = (inf A) ⊓ (inf B)`. -/218theorem isGLB_union {A B : Set X} {a b : X}219 (hA : IsGLB A a) (hB : IsGLB B b) : IsGLB (A ∪ B) (a ⊓ b) := by220 refine ⟨?_, ?_⟩221 · rintro z (hz | hz)222 · exact inf_le_left.trans (hA.1 hz)223 · exact inf_le_right.trans (hB.1 hz)224 · intro u hu225 have ha : u ≤ a := hA.2 fun z hz => hu (Or.inl hz)226 have hb : u ≤ b := hB.2 fun z hz => hu (Or.inr hz)227 exact le_inf ha hb228229end LatticeOrderedGroup230231section VectorLattice232233variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]234 [VectorLattice X]235236variable (x y : X)237238/-- A non-negative scalar distributes over `⊔`. -/239theorem nonneg_smul_sup (a : ℝ) (nonneg : a ≥ 0) :240 a • (x ⊔ y) = (a • x) ⊔ (a • y) := by241 by_cases h : a = 0242 · subst h243 simp only [zero_smul]; exact Eq.symm Std.max_self244 · apply le_antisymm245 · have hx : a⁻¹ • a • x ≤ a⁻¹ • (a • x ⊔ a • y) := by246 exact smul_le_smul_of_nonneg_left247 le_sup_left248 (by norm_num [nonneg])249 have hy : a⁻¹ • a • y ≤ a⁻¹ • (a • x ⊔ a • y) := by250 exact smul_le_smul_of_nonneg_left251 le_sup_right252 (by norm_num [nonneg])253 simp only [inv_smul_smul₀ h] at hx hy254 have hxy : x ⊔ y ≤ a⁻¹ • (a • x ⊔ a • y) :=255 sup_le hx hy256 calc257 a • (x ⊔ y) ≤ a • (a⁻¹ • (a • x ⊔ a • y)) := by258 exact smul_le_smul_of_nonneg_left hxy nonneg259 _ = a • x ⊔ a • y := by rw [smul_smul a a⁻¹ _]; norm_num [h];260 · have hx : a • x ≤ a • (x ⊔ y) :=261 smul_le_smul_of_nonneg_left le_sup_left nonneg262 have hy : a • y ≤ a • (x ⊔ y) :=263 smul_le_smul_of_nonneg_left le_sup_right nonneg264 exact sup_le hx hy265266/-- A non-negative scalar commutes with the positive part. -/267theorem posPart_smul_nonneg {a : ℝ} (ha : 0 ≤ a) (x : X) :268 (a • x)⁺ = a • x⁺ := by269 change (a • x) ⊔ 0 = a • (x ⊔ 0)270 rw [← smul_zero a, ← nonneg_smul_sup x 0 a ha, smul_zero]271272/-- A non-negative scalar distributes over suprema: `λ • sup A = sup (λ • A)`. -/273theorem isLUB_smul_of_nonneg {A : Set X} {a : X} {lam : ℝ} (hlam : 0 ≤ lam)274 (h : IsLUB A a) : IsLUB ((fun z => lam • z) '' A) (lam • a) := by275 refine ⟨?_, ?_⟩276 · rintro _ ⟨z, hz, rfl⟩277 exact smul_le_smul_of_nonneg_left (h.1 hz) hlam278 · intro u hu279 by_cases hl : lam = 0280 · subst hl; rw [zero_smul]281 rcases A.eq_empty_or_nonempty with rfl | ⟨z, hz⟩282 · have hmin : ∀ b : X, a ≤ b := fun b =>283 h.2 fun x hx => (Set.notMem_empty x hx).elim284 have h0a : 0 ≤ a :=285 (add_le_add_iff_left a).mp (by rw [add_zero]; exact hmin (a + a))286 exact h0a.trans (hmin u)287 · have : (0 : ℝ) • z ≤ u := hu ⟨z, hz, rfl⟩288 rwa [zero_smul] at this289 · have hlam_pos : 0 < lam := lt_of_le_of_ne hlam (Ne.symm hl)290 have hinv_nn : 0 ≤ lam⁻¹ := le_of_lt (inv_pos.mpr hlam_pos)291 have h_ub : lam⁻¹ • u ∈ upperBounds A := fun z hz => by292 have h1 : lam⁻¹ • (lam • z) ≤ lam⁻¹ • u :=293 smul_le_smul_of_nonneg_left (hu ⟨z, hz, rfl⟩) hinv_nn294 rwa [inv_smul_smul₀ hl] at h1295 have h4 : lam • a ≤ lam • (lam⁻¹ • u) :=296 smul_le_smul_of_nonneg_left (h.2 h_ub) hlam297 rwa [smul_inv_smul₀ hl] at h4298299/-- A non-negative scalar distributes over infima: `λ • inf A = inf (λ • A)`. -/300theorem isGLB_smul_of_nonneg {A : Set X} {a : X} {lam : ℝ} (hlam : 0 ≤ lam)301 (h : IsGLB A a) : IsGLB ((fun z => lam • z) '' A) (lam • a) := by302 refine ⟨?_, ?_⟩303 · rintro _ ⟨z, hz, rfl⟩304 exact smul_le_smul_of_nonneg_left (h.1 hz) hlam305 · intro u hu306 by_cases hl : lam = 0307 · subst hl; rw [zero_smul]308 rcases A.eq_empty_or_nonempty with rfl | ⟨z, hz⟩309 · have hmax : ∀ b : X, b ≤ a := fun b =>310 h.2 fun x hx => (Set.notMem_empty x hx).elim311 have ha0 : a ≤ 0 :=312 (add_le_add_iff_left a).mp (by rw [add_zero]; exact hmax (a + a))313 exact (hmax u).trans ha0314 · have : u ≤ (0 : ℝ) • z := hu ⟨z, hz, rfl⟩315 rwa [zero_smul] at this316 · have hlam_pos : 0 < lam := lt_of_le_of_ne hlam (Ne.symm hl)317 have hinv_nn : 0 ≤ lam⁻¹ := le_of_lt (inv_pos.mpr hlam_pos)318 have h_lb : lam⁻¹ • u ∈ lowerBounds A := fun z hz => by319 have h1 : lam⁻¹ • u ≤ lam⁻¹ • (lam • z) :=320 smul_le_smul_of_nonneg_left (hu ⟨z, hz, rfl⟩) hinv_nn321 rwa [inv_smul_smul₀ hl] at h1322 have h4 : lam • (lam⁻¹ • u) ≤ lam • a :=323 smul_le_smul_of_nonneg_left (h.2 h_lb) hlam324 rwa [smul_inv_smul₀ hl] at h4325326/-- A non-negative scalar distributes over `⊓`. -/327theorem nonneg_smul_inf (a : ℝ) (nonneg : a ≥ 0) :328 a • (x ⊓ y) = (a • x) ⊓ (a • y) := by329 calc330 a • (x ⊓ y) = (-1) • a • (- (x ⊓ y)) := by simp331 _ = (-1) • a • ((-x) ⊔ (-y)) := by rw [neg_inf]332 _ = (-1) • ((a • -x) ⊔ (a • -y)) := by rw [nonneg_smul_sup (-x) (-y) a nonneg]333 _ = - ((-a • x) ⊔ (-a • y)) := by simp334 _ = (a • x) ⊓ (a • y) := by rw [neg_sup]; simp335336/-- Scalar `sup` distributes over a non-negative element. -/337theorem sup_smul_nonneg (a b : ℝ) (h : 0 ≤ x) :338 (a ⊔ b) • x = (a • x) ⊔ (b • x) := by339 apply le_antisymm340 · cases max_choice a b with341 | inl h => rw [h]; exact le_sup_left342 | inr h => rw [h]; exact le_sup_right343 · apply sup_le344 · exact smul_le_smul_of_nonneg_right le_sup_left h345 · exact smul_le_smul_of_nonneg_right le_sup_right h346347/-- Scalar `inf` distributes over a non-negative element. -/348theorem inf_smul_nonneg (a b : ℝ) (h : 0 ≤ x) :349 (a ⊓ b) • x = (a • x) ⊓ (b • x) := by350 apply le_antisymm351 · apply le_inf352 · exact smul_le_smul_of_nonneg_right inf_le_left h353 · exact smul_le_smul_of_nonneg_right inf_le_right h354 · cases min_choice a b with355 | inl h => rw [h]; exact inf_le_left356 | inr h => rw [h]; exact inf_le_right357358/-- `|a • x| = |a| • |x|` in a vector lattice.359Extends the Mathlib result of the same name from total orders to lattice orders. -/360theorem abs_smul' (a : ℝ) : |a • x| = |a| • |x| := by361 by_cases ha : a ≥ 0362 · rw [abs_of_nonneg ha]363 rw [abs, abs]364 rw [nonneg_smul_sup x (-x) a ha]365 simp366 · have hna : a < 0 := by linarith367 rw [abs_of_neg hna]368 rw [abs, abs]369 rw [nonneg_smul_sup x (-x) (-a) (by linarith)]370 simp [sup_comm]371372section Archimedean373374/-- A lattice-ordered group is **Archimedean** (in the vector-lattice sense) when the only375non-negative element all of whose multiples are bounded is zero: `0 ≤ x` and `∀ n, n • x ≤ y`376imply `x = 0`. This is the standard Archimedean property for partially ordered groups; it is377weaker than Mathlib's `Archimedean` class, which is stated for linearly ordered monoids. -/378class IsVLArchimedean (X : Type*) [AddCommGroup X] [Lattice X]379 [IsOrderedAddMonoid X] : Prop where380 le_zero_of_forall_nsmul_le {x y : X} :381 (∀ n : ℕ, n • x ≤ y) → x ≤ 0382383private lemma nsmul_posPart_le_of_forall_nsmul_le {Y : Type*} [AddCommGroup Y] [Lattice Y]384 [IsOrderedAddMonoid Y] (x : Y) :385 ∀ (n : ℕ) (v : Y), (∀ k : ℕ, k ≤ n → k • x ≤ v) → n • (x ⊔ 0) ≤ v := by386 intro n387 induction n with388 | zero =>389 intro v h390 simpa using h 0 (le_refl 0)391 | succ n ih =>392 intro v h393 rw [succ_nsmul, add_sup, add_zero]394 refine sup_le ?_ (ih v fun k hk => h k (hk.trans (Nat.le_succ n)))395 rw [← le_sub_iff_add_le]396 refine ih (v - x) fun k hk => ?_397 rw [le_sub_iff_add_le, ← succ_nsmul]398 exact h (k + 1) (Nat.succ_le_succ hk)399400omit [VectorLattice X] in401/-- Constructor from the non-negative formulation of the Archimedean property. -/402theorem isVLArchimedean_of_eq_zero_of_nonneg_of_forall_nsmul_le403 (H : ∀ {x y : X}, 0 ≤ x → (∀ n : ℕ, n • x ≤ y) → x = 0) :404 IsVLArchimedean X := by405 refine ⟨fun {x y} h => ?_⟩406 have hsup : x ⊔ 0 = 0 :=407 H le_sup_right408 (fun n => nsmul_posPart_le_of_forall_nsmul_le x n y fun k _ => h k)409 exact sup_eq_right.mp hsup410411omit [VectorLattice X] in412/-- In a vector lattice, being Archimedean is equivalent to the condition that413`n • x ≤ y` for all `n : ℕ` implies `x ≤ 0`. -/414theorem isVLArchimedean_iff_le_zero_of_forall_nsmul_le :415 IsVLArchimedean X ↔ ∀ {x y : X}, (∀ n : ℕ, n • x ≤ y) → x ≤ 0 := by416 exact ⟨fun hArch _ _ h => hArch.le_zero_of_forall_nsmul_le h,417 fun H => ⟨fun {x y} h => H h⟩⟩418419namespace IsVLArchimedean420421omit [VectorLattice X] in422/-- Non-negative form of the Archimedean property. -/423theorem eq_zero_of_nonneg_of_forall_nsmul_le [IsVLArchimedean X] {x y : X}424 (hx : 0 ≤ x) (h : ∀ n : ℕ, n • x ≤ y) : x = 0 :=425 le_antisymm (IsVLArchimedean.le_zero_of_forall_nsmul_le h) hx426427end IsVLArchimedean428429/-- A vector lattice is Archimedean iff for every positive `u`, the infimum of430`(1/n) • u` over `n ≥ 1` equals `0`. -/431theorem isVLArchimedean_iff_isGLB_inv_smul :432 IsVLArchimedean X ↔433 ∀ u : X, 0 ≤ u →434 IsGLB {v : X | ∃ n : ℕ, 0 < n ∧ v = (n : ℝ)⁻¹ • u} 0 := by435 constructor436 · intro hArch u hu437 refine ⟨?_, ?_⟩438 · rintro _ ⟨n, _, rfl⟩439 exact smul_nonneg (by positivity) hu440 · intro w hw441 apply isVLArchimedean_iff_le_zero_of_forall_nsmul_le.mp hArch (y := u)442 intro n443 rcases Nat.eq_zero_or_pos n with rfl | hnpos444 · simpa using hu445 · have hwn : w ≤ (n : ℝ)⁻¹ • u := hw ⟨n, hnpos, rfl⟩446 have hn_nn : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg n447 have h1 : (n : ℝ) • w ≤ (n : ℝ) • ((n : ℝ)⁻¹ • u) :=448 smul_le_smul_of_nonneg_left hwn hn_nn449 rw [smul_inv_smul₀ (Nat.cast_ne_zero.mpr hnpos.ne')] at h1450 rwa [Nat.cast_smul_eq_nsmul] at h1451 · intro H452 apply isVLArchimedean_of_eq_zero_of_nonneg_of_forall_nsmul_le453 intro x y hx h454 set u := y ⊔ 0 with hu_def455 have hu : 0 ≤ u := le_sup_right456 have hx_lb : x ∈ lowerBounds {v : X | ∃ n : ℕ, 0 < n ∧ v = (n : ℝ)⁻¹ • u} := by457 rintro _ ⟨n, hnpos, rfl⟩458 have h1 : (n : ℝ) • x ≤ u := by459 rw [Nat.cast_smul_eq_nsmul]460 exact (h n).trans le_sup_left461 have hn_pos : (0 : ℝ) < n := Nat.cast_pos.mpr hnpos462 have h2 : (n : ℝ)⁻¹ • ((n : ℝ) • x) ≤ (n : ℝ)⁻¹ • u :=463 smul_le_smul_of_nonneg_left h1 (le_of_lt (inv_pos.mpr hn_pos))464 rwa [inv_smul_smul₀ hn_pos.ne'] at h2465 exact le_antisymm ((H u hu).2 hx_lb) hx466467variable [IsVLArchimedean X]468469omit [VectorLattice X] in470/-- An element whose absolute-value multiples are bounded must be zero. -/471theorem infinitesimal_eq_zero {x y : X}472 (h : ∀ n : ℕ, n • |x| ≤ y) : x = 0 := by473 have hab : |x| = 0 :=474 IsVLArchimedean.eq_zero_of_nonneg_of_forall_nsmul_le (abs_nonneg x) h475 exact (abs_eq_zero_iff_zero x).mp hab476477private lemma exists_real_eq_smul_of_linear_comparable478 (hcon : ∀ z : X, 0 ≤ z ∨ z ≤ 0)479 {u v : X} (hu : 0 ≤ u) (hu0 : u ≠ 0) (hv : 0 ≤ v) :480 ∃ r : ℝ, v = r • u := by481 let S : Set ℝ := {r | r • u ≤ v}482 have hS_ne : S.Nonempty := ⟨0, by simp [S, hv]⟩483 have hN : ∃ n : ℕ, ¬ (n : ℝ) • u ≤ v := by484 by_contra hna485 push Not at hna486 exact hu0 <| le_antisymm487 (isVLArchimedean_iff_le_zero_of_forall_nsmul_le.mp inferInstance488 (fun n => (Nat.cast_smul_eq_nsmul ℝ n u) ▸ hna n)) hu489 obtain ⟨N, hNp⟩ := hN490 have hS_bdd : BddAbove S := ⟨(N : ℝ), fun r hr => by491 by_contra hlt; push Not at hlt492 exact hNp ((smul_le_smul_of_nonneg_right hlt.le hu).trans hr)⟩493 set lam := sSup S with hlam_def494 refine ⟨lam, ?_⟩495 have heq : v - lam • u = 0 := by496 refine infinitesimal_eq_zero (y := u) fun m => ?_497 rcases Nat.eq_zero_or_pos m with rfl | hm_pos498 · simpa using hu499 have hm_real_pos : (0 : ℝ) < m := by exact_mod_cast hm_pos500 have hm_inv_pos : (0 : ℝ) < (m : ℝ)⁻¹ := inv_pos.mpr hm_real_pos501 have hUp : v - lam • u ≤ (m : ℝ)⁻¹ • u := by502 have h_not : ¬ (lam + (m : ℝ)⁻¹) • u ≤ v := fun hle =>503 (lt_add_of_pos_right lam hm_inv_pos).not_ge (le_csSup hS_bdd hle)504 have hvle : v ≤ (lam + (m : ℝ)⁻¹) • u := by505 rcases hcon (v - (lam + (m : ℝ)⁻¹) • u) with hnn | hnp506 · exact absurd (sub_nonneg.mp hnn) h_not507 · exact sub_nonpos.mp hnp508 rw [add_smul] at hvle509 exact sub_le_iff_le_add.mpr (by rwa [add_comm])510 have hLo : -((m : ℝ)⁻¹ • u) ≤ v - lam • u := by511 obtain ⟨r, hrS, hr⟩ : ∃ r ∈ S, lam - (m : ℝ)⁻¹ < r :=512 exists_lt_of_lt_csSup hS_ne (sub_lt_self lam hm_inv_pos)513 have h2 : (lam - (m : ℝ)⁻¹) • u ≤ v :=514 (smul_le_smul_of_nonneg_right hr.le hu).trans hrS515 rw [sub_smul] at h2516 rw [neg_le, neg_sub]517 have h3 : lam • u ≤ v + (m : ℝ)⁻¹ • u := sub_le_iff_le_add.mp h2518 rw [add_comm] at h3519 exact sub_le_iff_le_add.mpr h3520 have habs : |v - lam • u| ≤ (m : ℝ)⁻¹ • u :=521 abs_le'.mpr ⟨hUp, neg_le.mp hLo⟩522 have hm_nn : (0 : ℝ) ≤ m := hm_real_pos.le523 have hmabs : (m : ℝ) • |v - lam • u| ≤ (m : ℝ) • ((m : ℝ)⁻¹ • u) :=524 smul_le_smul_of_nonneg_left habs hm_nn525 rw [smul_inv_smul₀ hm_real_pos.ne'] at hmabs526 rwa [Nat.cast_smul_eq_nsmul] at hmabs527 exact sub_eq_zero.mp heq528529/-- If `X` is an Archimedean vector lattice with more than one dimension, then530there exists a vector in `X` which is neither positive nor negative. -/531theorem exists_not_nonneg_not_nonpos_of_one_lt_rank532 (h : 1 < Module.rank ℝ X) : ∃ x : X, ¬ 0 ≤ x ∧ ¬ x ≤ 0 := by533 by_contra hcon534 push Not at hcon535 have hcon' : ∀ x : X, 0 ≤ x ∨ x ≤ 0 :=536 fun x => (Classical.or_iff_not_imp_left).mpr (hcon x)537 haveI hnt : Nontrivial X :=538 (rank_pos_iff_nontrivial (R := ℝ) (M := X)).mp (lt_of_le_of_lt zero_le_one h)539 obtain ⟨x0, hx0⟩ : ∃ x : X, x ≠ 0 := exists_ne 0540 obtain ⟨y0, hxy⟩ := exists_linearIndependent_pair_of_one_lt_rank h hx0541 have hy0 : y0 ≠ 0 := by542 have := hxy.ne_zero 1543 simpa [Matrix.cons_val_one, Matrix.head_cons] using this544 obtain ⟨u, hu_eq, hu_pos, hu_nz⟩ : ∃ u : X, (u = x0 ∨ u = -x0) ∧ 0 ≤ u ∧ u ≠ 0 := by545 rcases hcon' x0 with hp | hp546 · exact ⟨x0, Or.inl rfl, hp, hx0⟩547 · exact ⟨-x0, Or.inr rfl, neg_nonneg.mpr hp, neg_ne_zero.mpr hx0⟩548 obtain ⟨v, hv_eq, hv_pos, _⟩ : ∃ v : X, (v = y0 ∨ v = -y0) ∧ 0 ≤ v ∧ v ≠ 0 := by549 rcases hcon' y0 with hp | hp550 · exact ⟨y0, Or.inl rfl, hp, hy0⟩551 · exact ⟨-y0, Or.inr rfl, neg_nonneg.mpr hp, neg_ne_zero.mpr hy0⟩552 obtain ⟨r, hr⟩ := exists_real_eq_smul_of_linear_comparable hcon' hu_pos hu_nz hv_pos553 have hxy_dep : ∃ s : ℝ, y0 = s • x0 := by554 obtain (hu1 : u = x0) | (hu1 : u = -x0) := hu_eq555 · obtain (hv1 : v = y0) | (hv1 : v = -y0) := hv_eq556 · rw [hu1, hv1] at hr; exact ⟨r, hr⟩557 · rw [hu1, hv1] at hr558 refine ⟨-r, ?_⟩559 have h1 : y0 = -(r • x0) := by rw [← hr, neg_neg]560 rw [h1, neg_smul]561 · obtain (hv1 : v = y0) | (hv1 : v = -y0) := hv_eq562 · rw [hu1, hv1] at hr563 refine ⟨-r, ?_⟩564 rw [hr, smul_neg, ← neg_smul]565 · rw [hu1, hv1] at hr566 refine ⟨r, ?_⟩567 rw [smul_neg] at hr568 rw [← neg_neg y0, hr, neg_neg]569 obtain ⟨s, hs⟩ := hxy_dep570 let g : Fin 2 → ℝ := ![s, -1]571 have key : ∑ i : Fin 2, g i • ![x0, y0] i = 0 := by572 change ∑ i : Fin 2, (![s, -1] : Fin 2 → ℝ) i • ![x0, y0] i = 0573 rw [Fin.sum_univ_two]574 simp only [Matrix.cons_val_zero, Matrix.cons_val_one]575 rw [hs, neg_one_smul]576 abel577 have h_false : g 1 = 0 := Fintype.linearIndependent_iff.mp hxy g key 1578 simp [g] at h_false579580end Archimedean581582end VectorLattice583