BanLat/Disjoint.lean
All source files · Download exact source
SHA-256: 51e351f291a15a8d88d42f17f787dada806f5dccc6e39775173dbe3fde9d54dc
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Normed67/-!8# Disjointness in vector lattices910Two elements `x`, `y` of a lattice-ordered group are **disjoint** when11`|x| ⊓ |y| = 0`, written `IsVLDisjoint x y`. This file collects the basic12theory: the symmetry and zero rules, the Birkhoff identity13`|x + y| = |x| + |y|`, the uniqueness of the positive/negative decomposition,14compatibility with scalar multiplication, monotonicity under absolute value,15closure under finite suprema and sums, and the finite-family identity16`|∑ i, α i • x i| = ∑ i, |α i| • |x i|` for pairwise-disjoint families. From17the last, a pairwise-disjoint family of non-zero vectors is linearly18independent over `ℝ`. Finally, in a normed vector lattice, a limit of a19pairwise-disjoint sequence is forced to be zero.20-/2122open scoped Topology23open Filter Finset2425section LatticeOrdered2627variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]2829/-! ### Definition and elementary lemmas -/3031/-- Two elements of a lattice-ordered group are **disjoint** when32`|x| ⊓ |y| = 0`. -/33def IsVLDisjoint (x y : X) : Prop := |x| ⊓ |y| = 03435omit [IsOrderedAddMonoid X] in36theorem isVLDisjoint_comm {x y : X} :37 IsVLDisjoint x y ↔ IsVLDisjoint y x := by38 unfold IsVLDisjoint; rw [inf_comm]3940/-- Zero is disjoint from every element. -/41theorem isVLDisjoint_zero_left (x : X) : IsVLDisjoint 0 x := by42 unfold IsVLDisjoint; simp [abs_zero]4344/-- Every element is disjoint from zero. -/45theorem isVLDisjoint_zero_right (x : X) : IsVLDisjoint x 0 :=46 isVLDisjoint_comm.mpr (isVLDisjoint_zero_left x)4748/-- Disjoint positive elements satisfy `x ⊓ y = 0`. -/49theorem inf_eq_zero_of_isVLDisjoint {x y : X} (hx : 0 ≤ x) (hy : 0 ≤ y)50 (h : IsVLDisjoint x y) : x ⊓ y = 0 := by51 unfold IsVLDisjoint at h; rwa [abs_of_nonneg hx, abs_of_nonneg hy] at h5253/-- If `x ⊓ y = 0` then `x` and `y` are disjoint. -/54theorem isVLDisjoint_of_inf_eq_zero {x y : X}55 (h : x ⊓ y = 0) : IsVLDisjoint x y := by56 have hx : 0 ≤ x := h ▸ inf_le_left57 have hy : 0 ≤ y := h ▸ inf_le_right58 unfold IsVLDisjoint; rwa [abs_of_nonneg hx, abs_of_nonneg hy]5960/-- Disjoint decomposition is unique: if `x = u₁ - v₁ = u₂ - v₂` with61`u₁ ⊥ v₁` and `u₂ ⊥ v₂` (all non-negative), then `u₁ = u₂` and62`v₁ = v₂`. -/63theorem isVLDisjoint_decomposition_unique {u₁ v₁ u₂ v₂ : X}64 (hu₁ : 0 ≤ u₁) (hv₁ : 0 ≤ v₁) (hu₂ : 0 ≤ u₂) (hv₂ : 0 ≤ v₂)65 (hd₁ : IsVLDisjoint u₁ v₁) (hd₂ : IsVLDisjoint u₂ v₂)66 (h : u₁ - v₁ = u₂ - v₂) : u₁ = u₂ ∧ v₁ = v₂ := by67 have h1 := inf_eq_zero_of_isVLDisjoint hu₁ hv₁ hd₁68 have h2 := inf_eq_zero_of_isVLDisjoint hu₂ hv₂ hd₂69 have eq1 : u₁ = (u₁ - v₁)⁺ :=70 uniqueness_posPart (u₁ - v₁) rfl h171 have eq2 : u₂ = (u₂ - v₂)⁺ :=72 uniqueness_posPart (u₂ - v₂) rfl h273 have hu : u₁ = u₂ := by rw [eq1, h, ← eq2]74 refine ⟨hu, ?_⟩75 have := h; rw [hu, sub_eq_add_neg, sub_eq_add_neg] at this76 exact neg_injective (add_left_cancel this)7778omit [IsOrderedAddMonoid X] in79private theorem inf_eq_zero_of_le_disjoint {a b c d : X}80 (ha : 0 ≤ a) (hb : 0 ≤ b) (hac : a ≤ c) (hbd : b ≤ d)81 (hcd : c ⊓ d = 0) : a ⊓ b = 0 :=82 le_antisymm (hcd ▸ inf_le_inf hac hbd) (le_inf ha hb)8384/-- If `x ⊥ y` then `|x + y| = |x| + |y|` (Birkhoff identity). -/85theorem abs_add_of_isVLDisjoint {x y : X} (h : IsVLDisjoint x y) :86 |x + y| = |x| + |y| := by87 have hd : |x| ⊓ |y| = 0 := h88 have hxp_yp : x⁺ ⊓ y⁺ = 0 := inf_eq_zero_of_le_disjoint89 (posPart_nonneg x) (posPart_nonneg y)90 (sup_le (le_abs_self x) (abs_nonneg x))91 (sup_le (le_abs_self y) (abs_nonneg y)) hd92 have hxp_yn : x⁺ ⊓ y⁻ = 0 := inf_eq_zero_of_le_disjoint93 (posPart_nonneg x) (negPart_nonneg y)94 (sup_le (le_abs_self x) (abs_nonneg x))95 (sup_le (neg_le_abs y) (abs_nonneg y)) hd96 have hxn_yp : x⁻ ⊓ y⁺ = 0 := inf_eq_zero_of_le_disjoint97 (negPart_nonneg x) (posPart_nonneg y)98 (sup_le (neg_le_abs x) (abs_nonneg x))99 (sup_le (le_abs_self y) (abs_nonneg y)) hd100 have hxn_yn : x⁻ ⊓ y⁻ = 0 := inf_eq_zero_of_le_disjoint101 (negPart_nonneg x) (negPart_nonneg y)102 (sup_le (neg_le_abs x) (abs_nonneg x))103 (sup_le (neg_le_abs y) (abs_nonneg y)) hd104 have hxn_xp : x⁻ ⊓ x⁺ = 0 := by105 rw [inf_comm]; exact posPart_inf_negPart_eq_zero x106 have hyn_yp : y⁻ ⊓ y⁺ = 0 := by107 rw [inf_comm]; exact posPart_inf_negPart_eq_zero y108 have term1 : (x⁺ + y⁺) ⊓ x⁻ = 0 := by109 apply le_antisymm _ (le_inf (add_nonneg (posPart_nonneg x) (posPart_nonneg y))110 (negPart_nonneg x))111 rw [inf_comm]112 calc x⁻ ⊓ (x⁺ + y⁺)113 ≤ x⁻ ⊓ x⁺ + x⁻ ⊓ y⁺ := inf_le_inf_add_inf_of_nonneg x⁻ x⁺ y⁺114 (negPart_nonneg x) (posPart_nonneg x) (posPart_nonneg y)115 _ = 0 := by rw [hxn_xp, hxn_yp, add_zero]116 have term2 : (x⁺ + y⁺) ⊓ y⁻ = 0 := by117 apply le_antisymm _ (le_inf (add_nonneg (posPart_nonneg x) (posPart_nonneg y))118 (negPart_nonneg y))119 rw [inf_comm]120 calc y⁻ ⊓ (x⁺ + y⁺)121 ≤ y⁻ ⊓ x⁺ + y⁻ ⊓ y⁺ := inf_le_inf_add_inf_of_nonneg y⁻ x⁺ y⁺122 (negPart_nonneg y) (posPart_nonneg x) (posPart_nonneg y)123 _ = 0 := by rw [inf_comm y⁻ x⁺, hxp_yn, hyn_yp, add_zero]124 have sum_disj : (x⁺ + y⁺) ⊓ (x⁻ + y⁻) = 0 := by125 apply le_antisymm _ (le_inf (add_nonneg (posPart_nonneg x) (posPart_nonneg y))126 (add_nonneg (negPart_nonneg x) (negPart_nonneg y)))127 calc (x⁺ + y⁺) ⊓ (x⁻ + y⁻)128 ≤ (x⁺ + y⁺) ⊓ x⁻ + (x⁺ + y⁺) ⊓ y⁻ :=129 inf_le_inf_add_inf_of_nonneg (x⁺ + y⁺) x⁻ y⁻130 (add_nonneg (posPart_nonneg x) (posPart_nonneg y))131 (negPart_nonneg x) (negPart_nonneg y)132 _ = 0 := by rw [term1, term2, add_zero]133 have hdec : x + y = (x⁺ + y⁺) - (x⁻ + y⁻) := by134 calc x + y = (x⁺ - x⁻) + (y⁺ - y⁻) := by135 rw [posPart_sub_negPart, posPart_sub_negPart]136 _ = (x⁺ + y⁺) - (x⁻ + y⁻) := by abel137 have hup := uniqueness_posPart (x + y) hdec sum_disj138 have hun : (x + y)⁻ = x⁻ + y⁻ := by139 have h3 := posPart_sub_negPart (x + y)140 rw [← hup] at h3141 have h4 : x⁺ + y⁺ - (x + y)⁻ = x⁺ + y⁺ - (x⁻ + y⁻) := by142 rw [h3, hdec]143 exact sub_right_injective h4144 calc |x + y| = (x + y)⁺ + (x + y)⁻ := (posPart_add_negPart (x + y)).symm145 _ = (x⁺ + y⁺) + (x⁻ + y⁻) := by rw [← hup, hun]146 _ = (x⁺ + x⁻) + (y⁺ + y⁻) := by abel147 _ = |x| + |y| := by rw [posPart_add_negPart, posPart_add_negPart]148149/-- If `x, y ≥ 0` and `x ⊥ y` then `|x ⊔ y| = |x| ⊔ |y|`. -/150theorem abs_sup_of_isVLDisjoint {x y : X} (hx : 0 ≤ x) (hy : 0 ≤ y)151 (_ : IsVLDisjoint x y) : |x ⊔ y| = |x| ⊔ |y| := by152 rw [abs_of_nonneg (le_sup_of_le_left hx), abs_of_nonneg hx, abs_of_nonneg hy]153154/-- The positive and negative parts of an element are disjoint. -/155theorem isVLDisjoint_posPart_negPart (x : X) : IsVLDisjoint x⁺ x⁻ :=156 isVLDisjoint_of_inf_eq_zero (posPart_inf_negPart_eq_zero x)157158/-- If `|z| ≤ |y|` and `x ⊥ y` then `x ⊥ z`. -/159theorem IsVLDisjoint.mono_right {x y z : X} (h : IsVLDisjoint x y)160 (hzy : |z| ≤ |y|) : IsVLDisjoint x z := by161 refine le_antisymm ?_ (le_inf (abs_nonneg _) (abs_nonneg _))162 calc |x| ⊓ |z| ≤ |x| ⊓ |y| := inf_le_inf_left _ hzy163 _ = 0 := h164165/-- If `|z| ≤ |x|` and `x ⊥ y` then `z ⊥ y`. -/166theorem IsVLDisjoint.mono_left {x y z : X} (h : IsVLDisjoint x y)167 (hzx : |z| ≤ |x|) : IsVLDisjoint z y :=168 isVLDisjoint_comm.mp ((isVLDisjoint_comm.mp h).mono_right hzx)169170/-! ### Sum of non-negative disjoint elements equals their supremum -/171172/-- For non-negative disjoint elements, `x + y = x ⊔ y`. -/173theorem add_eq_sup_of_isVLDisjoint_of_nonneg {x y : X}174 (hx : 0 ≤ x) (hy : 0 ≤ y) (h : IsVLDisjoint x y) : x + y = x ⊔ y := by175 have hinf : x ⊓ y = 0 := inf_eq_zero_of_isVLDisjoint hx hy h176 have := inf_add_sup x y177 rw [hinf, zero_add] at this178 exact this.symm179180/-- If a non-negative element is written as a sum of two disjoint elements,181then both summands are non-negative. -/182theorem nonneg_and_nonneg_of_isVLDisjoint_add_eq_of_nonneg183 {x y z : X} (hx : 0 ≤ x) (hyz : IsVLDisjoint y z) (hadd : y + z = x) :184 0 ≤ y ∧ 0 ≤ z := by185 have hsub : |y| + |z| - (y + z) = 0 := by186 calc187 |y| + |z| - (y + z) = |y + z| - (y + z) := by188 rw [abs_add_of_isVLDisjoint hyz]189 _ = |x| - x := by rw [hadd]190 _ = 0 := by rw [abs_of_nonneg hx, sub_self]191 have hy0 : |y| - y = 0 := by192 have hle : |y| - y ≤ |y| + |z| - (y + z) := by193 calc194 |y| - y ≤ (|y| - y) + (|z| - z) :=195 le_add_of_nonneg_right (sub_nonneg.mpr (le_abs_self z))196 _ = |y| + |z| - (y + z) := by abel197 exact le_antisymm (by rwa [hsub] at hle) (sub_nonneg.mpr (le_abs_self y))198 have hz0 : |z| - z = 0 := by199 calc200 |z| - z = 0 + (|z| - z) := by rw [zero_add]201 _ = (|y| - y) + (|z| - z) := by rw [hy0]202 _ = |y| + |z| - (y + z) := by abel203 _ = 0 := hsub204 constructor205 · rw [← sub_eq_zero.mp hy0]206 exact abs_nonneg y207 · rw [← sub_eq_zero.mp hz0]208 exact abs_nonneg z209210/-- If `x ⊥ y` then `|x| ⊔ |y| = |x| + |y|`. -/211theorem sup_abs_eq_add_abs_of_isVLDisjoint {x y : X}212 (h : IsVLDisjoint x y) : |x| ⊔ |y| = |x| + |y| := by213 have := inf_add_sup |x| |y|214 rw [show |x| ⊓ |y| = 0 from h, zero_add] at this215 exact this216217/-- If `x ⊥ y` then `|x + y| = |x| ⊔ |y|`. -/218theorem abs_add_eq_sup_abs_of_isVLDisjoint {x y : X}219 (h : IsVLDisjoint x y) : |x + y| = |x| ⊔ |y| := by220 rw [abs_add_of_isVLDisjoint h, sup_abs_eq_add_abs_of_isVLDisjoint h]221222/-! ### Disjointness with sups and sums on the right -/223224/-- If `x ⊥ y` and `x ⊥ z` then `x ⊥ y ⊔ z`. -/225theorem IsVLDisjoint.sup_right {x y z : X}226 (hy : IsVLDisjoint x y) (hz : IsVLDisjoint x z) :227 IsVLDisjoint x (y ⊔ z) := by228 have habs : |y ⊔ z| ≤ |y| + |z| := by229 rw [abs]230 refine sup_le ?_ ?_231 · exact sup_le ((le_abs_self y).trans232 (le_add_of_nonneg_right (abs_nonneg _)))233 ((le_abs_self z).trans (le_add_of_nonneg_left (abs_nonneg _)))234 · rw [neg_sup]235 exact inf_le_left.trans ((neg_le_abs y).trans236 (le_add_of_nonneg_right (abs_nonneg _)))237 refine le_antisymm ?_ (le_inf (abs_nonneg _) (abs_nonneg _))238 calc |x| ⊓ |y ⊔ z| ≤ |x| ⊓ (|y| + |z|) := inf_le_inf_left _ habs239 _ ≤ |x| ⊓ |y| + |x| ⊓ |z| := inf_le_inf_add_inf_of_nonneg _ _ _240 (abs_nonneg _) (abs_nonneg _) (abs_nonneg _)241 _ = 0 := by rw [hy, hz, add_zero]242243/-- If `x ⊥ y` and `x ⊥ z` then `x ⊥ y + z`. -/244theorem IsVLDisjoint.add_right {x y z : X}245 (hy : IsVLDisjoint x y) (hz : IsVLDisjoint x z) :246 IsVLDisjoint x (y + z) := by247 refine le_antisymm ?_ (le_inf (abs_nonneg _) (abs_nonneg _))248 calc |x| ⊓ |y + z| ≤ |x| ⊓ (|y| + |z|) := inf_le_inf_left _ (abs_add_le y z)249 _ ≤ |x| ⊓ |y| + |x| ⊓ |z| := inf_le_inf_add_inf_of_nonneg _ _ _250 (abs_nonneg _) (abs_nonneg _) (abs_nonneg _)251 _ = 0 := by rw [hy, hz, add_zero]252253/-- If `x ⊥ z` and `y ⊥ z` then `x ⊔ y ⊥ z`. -/254theorem IsVLDisjoint.sup_left {x y z : X}255 (hx : IsVLDisjoint x z) (hy : IsVLDisjoint y z) :256 IsVLDisjoint (x ⊔ y) z :=257 isVLDisjoint_comm.mp258 (IsVLDisjoint.sup_right (isVLDisjoint_comm.mp hx) (isVLDisjoint_comm.mp hy))259260/-- If `x ⊥ z` and `y ⊥ z` then `x + y ⊥ z`. -/261theorem IsVLDisjoint.add_left {x y z : X}262 (hx : IsVLDisjoint x z) (hy : IsVLDisjoint y z) :263 IsVLDisjoint (x + y) z :=264 isVLDisjoint_comm.mp265 (IsVLDisjoint.add_right (isVLDisjoint_comm.mp hx) (isVLDisjoint_comm.mp hy))266267/-! ### Disjoint pieces of an infimum -/268269/-- For any `x, y`, the elements `x - x ⊓ y` and `y - x ⊓ y` are non-negative270and disjoint. -/271theorem isVLDisjoint_sub_inf (x y : X) :272 IsVLDisjoint (x - x ⊓ y) (y - x ⊓ y) := by273 have h1 : x - x ⊓ y = (x - y)⁺ := sub_inf_eq_posPart x y274 have h2 : y - x ⊓ y = (x - y)⁻ := by275 rw [inf_comm, sub_inf_eq_posPart, negPart_def, neg_sub, posPart_def]276 rw [h1, h2]277 exact isVLDisjoint_posPart_negPart (x - y)278279/-! ### Finite disjoint sums -/280281private lemma isVLDisjoint_finset_sum {ι : Type*} {s : Finset ι} {x : X} {f : ι → X}282 (h : ∀ i ∈ s, IsVLDisjoint x (f i)) : IsVLDisjoint x (∑ i ∈ s, f i) := by283 classical284 induction s using Finset.induction_on with285 | empty => simpa using isVLDisjoint_zero_right x286 | insert a s ha ih =>287 rw [Finset.sum_insert ha]288 refine (h a (Finset.mem_insert_self a s)).add_right ?_289 exact ih (fun i hi => h i (Finset.mem_insert_of_mem hi))290291private lemma sum_eq_sup'_aux {ι : Type*} {s : Finset ι} (hs : s.Nonempty) (f : ι → X)292 (hnn : ∀ i ∈ s, 0 ≤ f i)293 (hdisj : (s : Set ι).Pairwise fun i j => IsVLDisjoint (f i) (f j)) :294 ∑ i ∈ s, f i = s.sup' hs f := by295 classical296 induction hs using Finset.Nonempty.cons_induction with297 | singleton a => simp298 | cons a s ha hs ih =>299 rw [Finset.sum_cons, Finset.sup'_cons hs f]300 have mem_cons_of : ∀ i ∈ s, i ∈ Finset.cons a s ha :=301 fun i hi => Finset.mem_cons.mpr (Or.inr hi)302 have hnn_s : ∀ i ∈ s, 0 ≤ f i := fun i hi => hnn i (mem_cons_of i hi)303 have hnn_a : 0 ≤ f a := hnn a (Finset.mem_cons.mpr (Or.inl rfl))304 have hdisj_s : (s : Set ι).Pairwise fun i j => IsVLDisjoint (f i) (f j) := by305 intro i hi j hj hij306 exact hdisj (mem_cons_of i hi) (mem_cons_of j hj) hij307 rw [← ih hnn_s hdisj_s]308 have hsum_nn : 0 ≤ ∑ i ∈ s, f i := Finset.sum_nonneg hnn_s309 have hdisj_sum : IsVLDisjoint (f a) (∑ i ∈ s, f i) := by310 apply isVLDisjoint_finset_sum311 intro i hi312 have hne_ai : a ≠ i := fun h => ha (h ▸ hi)313 exact hdisj (Finset.mem_cons.mpr (Or.inl rfl)) (mem_cons_of i hi) hne_ai314 exact add_eq_sup_of_isVLDisjoint_of_nonneg hnn_a hsum_nn hdisj_sum315316/-- For a pairwise-disjoint family of non-negative elements, the finite sum317equals the supremum. -/318theorem sum_eq_sup_of_pairwise_isVLDisjoint_of_nonneg {n : ℕ} {f : Fin n → X}319 (hne : 0 < n) (hnn : ∀ i, 0 ≤ f i)320 (hdisj : Pairwise fun i j => IsVLDisjoint (f i) (f j)) :321 ∑ i, f i = Finset.univ.sup' (Finset.univ_nonempty_iff.mpr322 ⟨⟨0, hne⟩⟩) f := by323 apply sum_eq_sup'_aux324 · intro i _; exact hnn i325 · intro i _ j _ hij; exact hdisj hij326327end LatticeOrdered328329section VectorLattice330331variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]332 [VectorLattice X]333334/-! ### Scalar multiples preserve disjointness -/335336/-- Scaling a non-negative disjoint pair preserves disjointness. -/337private lemma disjoint_smul_nonneg {x y : X} (a : ℝ) (nonneg : 0 ≤ a)338 (h : x ⊓ y = 0) : (a • x) ⊓ y = 0 := by339 let aux (x y : X) (h : x ⊓ y = 0) (a : ℝ)340 (nonneg : 0 ≤ a) (hone : a ≤ 1) : (a • x) ⊓ y = 0 := by341 have xnonneg : 0 ≤ x := by rw [← h]; exact inf_le_left342 have ynonneg : 0 ≤ y := by rw [← h]; exact inf_le_right343 apply le_antisymm344 · calc345 a • x ⊓ y ≤ (1 : ℝ) • x ⊓ y := by346 apply inf_le_inf347 · exact smul_le_smul_of_nonneg_right hone xnonneg348 · exact le_refl y349 _ = 0 := by simp [h]350 · exact le_inf (smul_nonneg nonneg xnonneg) ynonneg351 have hbig (hone : ¬ a ≤ 1) : (a • x) ⊓ y = 0 := by352 push Not at hone353 suffices hsuf : x ⊓ (a⁻¹ • y) = 0 from by354 symm355 calc356 0 = a • ( x ⊓ (a⁻¹ • y) ):= by rw [hsuf, smul_zero]357 _ = (a • x ⊓ a • a⁻¹ • y) := nonneg_smul_inf x (a⁻¹ • y) a nonneg358 _ = (a • x) ⊓ y := by rw [smul_smul]; field_simp [hone]; simp359 rw [inf_comm]; rw [inf_comm] at h360 refine aux y x h a⁻¹ ?_ ?_361 · exact inv_nonneg.mpr nonneg362 · field_simp; exact le_of_lt hone363 by_cases hone : a ≤ 1364 · exact aux x y h a nonneg hone365 · exact hbig hone366367/-- Scalar multiplication on the left preserves disjointness. -/368theorem IsVLDisjoint.smul_left {x y : X} (h : IsVLDisjoint x y) (a : ℝ) :369 IsVLDisjoint (a • x) y := by370 change |a • x| ⊓ |y| = 0371 rw [abs_smul']372 exact disjoint_smul_nonneg (|a| : ℝ) (abs_nonneg a) h373374/-- Scalar multiplication on the right preserves disjointness. -/375theorem IsVLDisjoint.smul_right {x y : X} (h : IsVLDisjoint x y) (a : ℝ) :376 IsVLDisjoint x (a • y) :=377 isVLDisjoint_comm.mp ((isVLDisjoint_comm.mp h).smul_left a)378379/-- Two non-zero disjoint vectors exist in any Archimedean vector lattice of380`ℝ`-rank greater than one. -/381theorem exists_pair_ne_zero_isVLDisjoint [IsVLArchimedean X]382 (h : 1 < Module.rank ℝ X) :383 ∃ u v : X, u ≠ 0 ∧ v ≠ 0 ∧ IsVLDisjoint u v := by384 obtain ⟨x, hxp, hxn⟩ := exists_not_nonneg_not_nonpos_of_one_lt_rank h385 refine ⟨x⁺, x⁻, ?_, ?_, isVLDisjoint_posPart_negPart x⟩386 · exact fun h => hxn (posPart_eq_zero.mp h)387 · exact fun h => hxp (negPart_eq_zero.mp h)388389/-! ### Disjoint positive parts from scalar multiples -/390391/-- For any `x, y` and `λ > 0`, the positive parts `(x - λ • y)⁺` and392`(y - λ⁻¹ • x)⁺` are disjoint. -/393theorem isVLDisjoint_posPart_sub_smul (x y : X) {lam : ℝ} (hlam : 0 < lam) :394 IsVLDisjoint (x - lam • y)⁺ (y - lam⁻¹ • x)⁺ := by395 have hne : lam ≠ 0 := ne_of_gt hlam396 have hinv : (0 : ℝ) ≤ lam⁻¹ := le_of_lt (inv_pos.mpr hlam)397 have heq : (y - lam⁻¹ • x)⁺ = lam⁻¹ • (x - lam • y)⁻ := by398 rw [negPart_def, nonneg_smul_sup _ _ _ hinv, smul_zero, posPart_def,399 neg_sub, smul_sub, smul_smul, inv_mul_cancel₀ hne, one_smul]400 rw [heq]401 exact (isVLDisjoint_posPart_negPart (x - lam • y)).smul_right lam⁻¹402403/-! ### Finite disjoint families with scalars -/404405private lemma abs_sum_finset {ι : Type*} (s : Finset ι) (x : ι → X) (α : ι → ℝ)406 (hdisj : (s : Set ι).Pairwise fun i j => IsVLDisjoint (x i) (x j)) :407 |∑ i ∈ s, α i • x i| = ∑ i ∈ s, |α i| • |x i| := by408 classical409 induction s using Finset.induction_on with410 | empty => simp411 | insert a s ha ih =>412 have hdisj_s : (s : Set ι).Pairwise fun i j => IsVLDisjoint (x i) (x j) := by413 intro i hi j hj hij414 exact hdisj (Finset.mem_insert_of_mem hi) (Finset.mem_insert_of_mem hj) hij415 rw [Finset.sum_insert ha, Finset.sum_insert ha]416 have hdisj_head : IsVLDisjoint (α a • x a) (∑ i ∈ s, α i • x i) := by417 apply isVLDisjoint_finset_sum418 intro i hi419 have hne_ai : a ≠ i := fun h => ha (h ▸ hi)420 exact ((hdisj (Finset.mem_insert_self a s)421 (Finset.mem_insert_of_mem hi) hne_ai).smul_left (α a)).smul_right (α i)422 rw [abs_add_of_isVLDisjoint hdisj_head, abs_smul', ih hdisj_s]423424/-- For a pairwise-disjoint family and arbitrary scalars,425`|∑ i, α i • x i| = ∑ i, |α i| • |x i|`. -/426theorem abs_sum_of_pairwise_isVLDisjoint {n : ℕ} {x : Fin n → X} {α : Fin n → ℝ}427 (hdisj : Pairwise fun i j => IsVLDisjoint (x i) (x j)) :428 |∑ i, α i • x i| = ∑ i, |α i| • |x i| :=429 abs_sum_finset Finset.univ x α (fun _ _ _ _ hij => hdisj hij)430431/-- For a pairwise-disjoint family of non-negative elements and non-negative432scalars, `∑ i, α i • x i = ⨆ i, α i • x i` (with the sup taken over a433non-empty index). -/434theorem sup_smul_eq_sum_of_pairwise_isVLDisjoint_of_nonneg {n : ℕ}435 {x : Fin n → X} {α : Fin n → ℝ} (hne : 0 < n)436 (hnn : ∀ i, 0 ≤ x i) (hα : ∀ i, 0 ≤ α i)437 (hdisj : Pairwise fun i j => IsVLDisjoint (x i) (x j)) :438 ∑ i, α i • x i = Finset.univ.sup' (Finset.univ_nonempty_iff.mpr439 ⟨⟨0, hne⟩⟩) (fun i => α i • x i) := by440 refine sum_eq_sup_of_pairwise_isVLDisjoint_of_nonneg hne441 (fun i => smul_nonneg (hα i) (hnn i)) ?_442 intro i j hij443 exact ((hdisj hij).smul_left (α i)).smul_right (α j)444445/-- A pairwise-disjoint family of non-zero vectors is linearly independent446over `ℝ`. -/447theorem linearIndependent_of_pairwise_isVLDisjoint {n : ℕ} {x : Fin n → X}448 (hne : ∀ i, x i ≠ 0)449 (hdisj : Pairwise fun i j => IsVLDisjoint (x i) (x j)) :450 LinearIndependent ℝ x := by451 rw [Fintype.linearIndependent_iff]452 intro α hsum i453 have habs : |∑ i, α i • x i| = ∑ i, |α i| • |x i| :=454 abs_sum_of_pairwise_isVLDisjoint hdisj455 rw [hsum, abs_zero] at habs456 have hnn : ∀ j ∈ (Finset.univ : Finset (Fin n)), 0 ≤ |α j| • |x j| :=457 fun j _ => smul_nonneg (abs_nonneg _) (abs_nonneg _)458 have hzero : |α i| • |x i| = 0 :=459 (Finset.sum_eq_zero_iff_of_nonneg hnn).mp habs.symm i (Finset.mem_univ i)460 by_contra hα461 have habs_ne : |α i| ≠ 0 := fun h => hα (abs_eq_zero.mp h)462 have hxi : |x i| = 0 := by463 have h2 : |α i|⁻¹ • (|α i| • |x i|) = |α i|⁻¹ • (0 : X) := by rw [hzero]464 rwa [smul_smul, inv_mul_cancel₀ habs_ne, one_smul, smul_zero] at h2465 exact hne i ((abs_eq_zero_iff_zero (x i)).mp hxi)466467/-! ### Pairwise disjoint families and maximality468469A subset of a vector lattice is **pairwise disjoint** when distinct members470are vector-lattice disjoint, and **maximal** when it is not properly471contained in any strictly larger pairwise disjoint subset. Every vector472lattice admits a maximal disjoint family consisting of strictly positive473vectors, by Zorn's lemma. -/474475/-- A subset of `X` is **pairwise disjoint** when it does not contain `0`476and distinct members are vector-lattice disjoint. -/477def IsDisjointSet (Λ : Set X) : Prop :=478 0 ∉ Λ ∧ ∀ ⦃a⦄, a ∈ Λ → ∀ ⦃b⦄, b ∈ Λ → a ≠ b → IsVLDisjoint a b479480/-- A **maximal disjoint family** in `X` is a pairwise disjoint set that is481not properly contained in any strictly larger pairwise disjoint subset of482`X`. The order is by inclusion (not refinement). -/483def IsMaximalDisjoint (Λ : Set X) : Prop :=484 Maximal IsDisjointSet Λ485486omit [VectorLattice X] in487/-- A pairwise disjoint family of strictly positive elements is maximal iff488the only element disjoint from every member of the family is `0`. -/489theorem isMaximalDisjoint_iff_forall_eq_zero {Λ : Set X}490 (_hpos : ∀ x ∈ Λ, 0 < x) (hdis : IsDisjointSet Λ) :491 IsMaximalDisjoint Λ ↔ ∀ x : X, (∀ a ∈ Λ, IsVLDisjoint x a) → x = 0 := by492 refine ⟨?_, ?_⟩493 · intro hmax x hx494 by_contra hxne495 have habs_ne : |x| ≠ 0 := fun h => hxne ((abs_eq_zero_iff_zero x).mp h)496 have habs_pos : 0 < |x| := lt_of_le_of_ne (abs_nonneg x) (Ne.symm habs_ne)497 have habs_disj : ∀ a ∈ Λ, IsVLDisjoint |x| a := fun a ha =>498 (hx a ha).mono_left (abs_of_nonneg (abs_nonneg x)).le499 set Λ' : Set X := insert |x| Λ with hΛ'_def500 have hΛ'_dis : IsDisjointSet Λ' := by501 refine ⟨?_, ?_⟩502 · rintro (h0 | h0)503 · exact habs_ne h0.symm504 · exact hdis.1 h0505 · intro a ha b hb hab506 rcases ha with rfl | ha507 · rcases hb with rfl | hb508 · exact (hab rfl).elim509 · exact habs_disj b hb510 · rcases hb with rfl | hb511 · exact isVLDisjoint_comm.mp (habs_disj a ha)512 · exact hdis.2 ha hb hab513 have hsub : Λ ⊆ Λ' := Set.subset_insert _ _514 have hsub' : Λ' ⊆ Λ := hmax.2 hΛ'_dis hsub515 have hxinΛ : |x| ∈ Λ := hsub' (Set.mem_insert _ _)516 have hself : |x| ⊓ |(|x|)| = 0 := hx |x| hxinΛ517 rw [abs_of_nonneg (abs_nonneg x), inf_idem] at hself518 exact habs_ne hself519 · intro hyp520 refine ⟨hdis, ?_⟩521 intro Λ' hΛ' hsub y hy522 by_contra hyΛ523 have hyΛ : y ∉ Λ := hyΛ524 have hy_disj : ∀ a ∈ Λ, IsVLDisjoint y a := by525 intro a ha526 have hane : y ≠ a := fun h => hyΛ (h.symm ▸ ha)527 exact hΛ'.2 hy (hsub ha) hane528 have hy0 : y = 0 := hyp y hy_disj529 exact hΛ'.1 (hy0 ▸ hy)530531/-- **Existence of a maximal disjoint family of positive vectors.** Every532lattice-ordered additive group admits a maximal disjoint family whose elements533are all strictly positive. -/534theorem exists_isMaximalDisjoint_pos (X : Type*) [AddCommGroup X] [Lattice X]535 [IsOrderedAddMonoid X] :536 ∃ Λ : Set X, IsMaximalDisjoint Λ ∧ ∀ x ∈ Λ, 0 < x := by537 let 𝒞 : Set (Set X) := {S | IsDisjointSet S ∧ ∀ x ∈ S, 0 < x}538 have hZorn : ∀ c ⊆ 𝒞, IsChain (· ⊆ ·) c → ∃ ub ∈ 𝒞, ∀ s ∈ c, s ⊆ ub := by539 intro c hc hchain540 refine ⟨⋃₀ c, ⟨⟨?_, ?_⟩, ?_⟩, fun s hs => Set.subset_sUnion_of_mem hs⟩541 · rintro ⟨S, hS, h0⟩542 exact (hc hS).1.1 h0543 · intro a ha b hb hab544 obtain ⟨Sa, hSa, haSa⟩ := ha545 obtain ⟨Sb, hSb, hbSb⟩ := hb546 rcases hchain.total hSa hSb with hSab | hSab547 · exact (hc hSb).1.2 (hSab haSa) hbSb hab548 · exact (hc hSa).1.2 haSa (hSab hbSb) hab549 · rintro x ⟨S, hS, hxS⟩550 exact (hc hS).2 x hxS551 obtain ⟨Λ, hΛ⟩ := zorn_subset 𝒞 hZorn552 refine ⟨Λ, ⟨hΛ.prop.1, ?_⟩, hΛ.prop.2⟩553 intro Λ' hΛ' hsub y hy554 by_contra hyΛ555 have hyΛ : y ∉ Λ := hyΛ556 have hy_ne : y ≠ 0 := fun h => hΛ'.1 (h ▸ hy)557 have habsy_ne : |y| ≠ 0 := fun h => hy_ne ((abs_eq_zero_iff_zero y).mp h)558 have habsy_pos : 0 < |y| := lt_of_le_of_ne (abs_nonneg y) (Ne.symm habsy_ne)559 have hy_disj : ∀ a ∈ Λ, IsVLDisjoint y a := by560 intro a ha561 have hane : y ≠ a := fun h => hyΛ (h.symm ▸ ha)562 exact hΛ'.2 hy (hsub ha) hane563 set Λ'' : Set X := insert |y| Λ564 have hΛ''_in : Λ'' ∈ 𝒞 := by565 refine ⟨⟨?_, ?_⟩, ?_⟩566 · rintro (h0 | h0)567 · exact habsy_ne h0.symm568 · exact hΛ.prop.1.1 h0569 · intro a ha b hb hab570 rcases ha with rfl | ha571 · rcases hb with rfl | hb572 · exact (hab rfl).elim573 · exact (hy_disj b hb).mono_left (abs_of_nonneg (abs_nonneg y)).le574 · rcases hb with rfl | hb575 · exact isVLDisjoint_comm.mp576 ((hy_disj a ha).mono_left (abs_of_nonneg (abs_nonneg y)).le)577 · exact hΛ.prop.1.2 ha hb hab578 · rintro x (rfl | hx)579 · exact habsy_pos580 · exact hΛ.prop.2 x hx581 have hsub'' : Λ ⊆ Λ'' := Set.subset_insert _ _582 have hsub''' : Λ'' ⊆ Λ := hΛ.2 hΛ''_in hsub''583 have habs_in : |y| ∈ Λ := hsub''' (Set.mem_insert _ _)584 by_cases hyabs : y = |y|585 · exact hyΛ (hyabs ▸ habs_in)586 · have hd : |y| ⊓ |(|y|)| = 0 := hΛ'.2 hy (hsub habs_in) hyabs587 rw [abs_of_nonneg (abs_nonneg y), inf_idem] at hd588 exact habsy_ne hd589590end VectorLattice591592/-! ### Disjoint sequences in normed vector lattices -/593594/-- In a normed vector lattice, a limit of a pairwise-disjoint sequence is595zero. -/596theorem eq_zero_of_pairwise_isVLDisjoint_tendsto {Y : Type*}597 [NormedAddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y]598 [NormedVectorLattice Y] {u : ℕ → Y} {x : Y}599 (hdisj : Pairwise fun i j => IsVLDisjoint (u i) (u j))600 (hlim : Tendsto u atTop (𝓝 x)) : x = 0 := by601 have habs_bound : ∀ n m, n ≠ m → |u n| ≤ |u n - u m| := by602 intro n m hnm603 have hdnm : IsVLDisjoint (u n) (-u m) := by604 change |u n| ⊓ |-u m| = 0605 rw [abs_neg]; exact hdisj hnm606 rw [sub_eq_add_neg, abs_add_of_isVLDisjoint hdnm, abs_neg]607 exact le_add_of_nonneg_right (abs_nonneg _)608 have hnorm_bound : ∀ n m, n ≠ m → ‖u n‖ ≤ ‖u n - u m‖ :=609 fun n m hnm => norm_le_norm_of_abs_le_abs (habs_bound n m hnm)610 have hnorm_limit : ∀ n, ‖u n‖ ≤ ‖u n - x‖ := by611 intro n612 have hrhs : Tendsto (fun m => ‖u n - u m‖) atTop (𝓝 ‖u n - x‖) :=613 (continuous_norm.tendsto _).comp (hlim.const_sub _)614 refine ge_of_tendsto hrhs ?_615 filter_upwards [eventually_ne_atTop n] with m hm616 exact hnorm_bound n m hm.symm617 have hlhs_tendsto : Tendsto (fun n => ‖u n‖) atTop (𝓝 ‖x‖) :=618 (continuous_norm.tendsto _).comp hlim619 have hrhs_zero : Tendsto (fun n => ‖u n - x‖) atTop (𝓝 0) := by620 have h1 : Tendsto (fun n => u n - x) atTop (𝓝 0) := by621 simpa using hlim.sub_const x622 have h := (continuous_norm.tendsto (0 : Y)).comp h1623 have h' : Tendsto (fun n => ‖u n - x‖) atTop (𝓝 ‖(0 : Y)‖) :=624 h.congr' <| Eventually.of_forall fun n ↦ by simp only [Function.comp_apply]625 simpa only [norm_zero] using h'626 have hxnn : ‖x‖ ≤ 0 :=627 le_of_tendsto_of_tendsto' hlhs_tendsto hrhs_zero hnorm_limit628 exact norm_le_zero_iff.mp hxnn629