Disjointness in vector lattices

Two elements x, y of a lattice-ordered group are disjoint when |x| ⊓ |y| = 0, written IsVLDisjoint x y. This file collects the basic theory: the symmetry and zero rules, the Birkhoff identity |x + y| = |x| + |y|, the uniqueness of the positive/negative decomposition, compatibility with scalar multiplication, monotonicity under absolute value, closure under finite suprema and sums, and the finite-family identity |∑ i, α i • x i| = ∑ i, |α i| • |x i| for pairwise-disjoint families. From the last, a pairwise-disjoint family of non-zero vectors is linearly independent over ℝ. Finally, in a normed vector lattice, a limit of a pairwise-disjoint sequence is forced to be zero.

Definition and elementary lemmas

def IsVLDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] (x y : X) : Prop

Two elements of a lattice-ordered group are disjoint when |x| ⊓ |y| = 0.

Equations

• IsVLDisjoint x y = (|x| ⊓ |y| = 0)

theorem isVLDisjoint_comm {X : Type u_1} [AddCommGroup X] [Lattice X] {x y : X} : IsVLDisjoint x y ↔ IsVLDisjoint y x

theorem isVLDisjoint_zero_left {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x : X) : IsVLDisjoint 0 x

Zero is disjoint from every element.

theorem isVLDisjoint_zero_right {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x : X) : IsVLDisjoint x 0

Every element is disjoint from zero.

theorem inf_eq_zero_of_isVLDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y : X} (hx : 0 ≤ x) (hy : 0 ≤ y) (h : IsVLDisjoint x y) : x ⊓ y = 0

Disjoint positive elements satisfy x ⊓ y = 0.

theorem isVLDisjoint_of_inf_eq_zero {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y : X} (h : x ⊓ y = 0) : IsVLDisjoint x y

If x ⊓ y = 0 then x and y are disjoint.

theorem isVLDisjoint_decomposition_unique {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {u₁ v₁ u₂ v₂ : X} (hu₁ : 0 ≤ u₁) (hv₁ : 0 ≤ v₁) (hu₂ : 0 ≤ u₂) (hv₂ : 0 ≤ v₂) (hd₁ : IsVLDisjoint u₁ v₁) (hd₂ : IsVLDisjoint u₂ v₂) (h : u₁ - v₁ = u₂ - v₂) : u₁ = u₂ ∧ v₁ = v₂

Disjoint decomposition is unique: if x = u₁ - v₁ = u₂ - v₂ with u₁ ⊥ v₁ and u₂ ⊥ v₂ (all non-negative), then u₁ = u₂ and v₁ = v₂.

theorem abs_add_of_isVLDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y : X} (h : IsVLDisjoint x y) : |x + y| = |x| + |y|

If x ⊥ y then |x + y| = |x| + |y| (Birkhoff identity).

theorem abs_sup_of_isVLDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y : X} (hx : 0 ≤ x) (hy : 0 ≤ y) : |x ⊔ y| = |x| ⊔ |y|

Absolute value preserves the supremum of nonnegative elements.

theorem isVLDisjoint_posPart_negPart {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x : X) : IsVLDisjoint x⁺ x⁻

The positive and negative parts of an element are disjoint.

theorem IsVLDisjoint.mono_right {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y z : X} (h : IsVLDisjoint x y) (hzy : |z| ≤ |y|) : IsVLDisjoint x z

If |z| ≤ |y| and x ⊥ y then x ⊥ z.

theorem IsVLDisjoint.mono_left {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y z : X} (h : IsVLDisjoint x y) (hzx : |z| ≤ |x|) : IsVLDisjoint z y

If |z| ≤ |x| and x ⊥ y then z ⊥ y.

Sum of non-negative disjoint elements equals their supremum

theorem add_eq_sup_of_isVLDisjoint_of_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y : X} (hx : 0 ≤ x) (hy : 0 ≤ y) (h : IsVLDisjoint x y) : x + y = x ⊔ y

For non-negative disjoint elements, x + y = x ⊔ y.

theorem nonneg_and_nonneg_of_isVLDisjoint_add_eq_of_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y z : X} (hx : 0 ≤ x) (hyz : IsVLDisjoint y z) (hadd : y + z = x) : 0 ≤ y ∧ 0 ≤ z

If a non-negative element is written as a sum of two disjoint elements, then both summands are non-negative.

theorem sup_abs_eq_add_abs_of_isVLDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y : X} (h : IsVLDisjoint x y) : |x| ⊔ |y| = |x| + |y|

If x ⊥ y then |x| ⊔ |y| = |x| + |y|.

theorem abs_add_eq_sup_abs_of_isVLDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y : X} (h : IsVLDisjoint x y) : |x + y| = |x| ⊔ |y|

If x ⊥ y then |x + y| = |x| ⊔ |y|.

Disjointness with sups and sums on the right

theorem IsVLDisjoint.sup_right {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y z : X} (hy : IsVLDisjoint x y) (hz : IsVLDisjoint x z) : IsVLDisjoint x (y ⊔ z)

If x ⊥ y and x ⊥ z then x ⊥ y ⊔ z.

theorem IsVLDisjoint.add_right {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y z : X} (hy : IsVLDisjoint x y) (hz : IsVLDisjoint x z) : IsVLDisjoint x (y + z)

If x ⊥ y and x ⊥ z then x ⊥ y + z.

theorem IsVLDisjoint.sup_left {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y z : X} (hx : IsVLDisjoint x z) (hy : IsVLDisjoint y z) : IsVLDisjoint (x ⊔ y) z

If x ⊥ z and y ⊥ z then x ⊔ y ⊥ z.

theorem IsVLDisjoint.add_left {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {x y z : X} (hx : IsVLDisjoint x z) (hy : IsVLDisjoint y z) : IsVLDisjoint (x + y) z

If x ⊥ z and y ⊥ z then x + y ⊥ z.

Disjoint pieces of an infimum

theorem isVLDisjoint_sub_inf {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (x y : X) : IsVLDisjoint (x - x ⊓ y) (y - x ⊓ y)

For any x, y, the elements x - x ⊓ y and y - x ⊓ y are non-negative and disjoint.

Finite disjoint sums

theorem isVLDisjoint_finset_sum {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {ι : Type u_2} {s : Finset ι} {x : X} {f : ι → X} (h : ∀ i ∈ s, IsVLDisjoint x (f i)) : IsVLDisjoint x (∑ i ∈ s, f i)

A sum of elements disjoint from a fixed element remains disjoint from it.

theorem sum_eq_sup_of_pairwise_isVLDisjoint_of_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {n : ℕ} {f : Fin n → X} (hne : 0 < n) (hnn : ∀ (i : Fin n), 0 ≤ f i) (hdisj : Pairwise fun (i j : Fin n) => IsVLDisjoint (f i) (f j)) : ∑ i : Fin n, f i = Finset.univ.sup' ⋯ f

For a pairwise-disjoint family of non-negative elements, the finite sum equals the supremum.

Scalar multiples preserve disjointness

theorem IsVLDisjoint.smul_left {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {x y : X} (h : IsVLDisjoint x y) (a : ℝ) : IsVLDisjoint (a • x) y

Scalar multiplication on the left preserves disjointness.

theorem IsVLDisjoint.smul_right {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {x y : X} (h : IsVLDisjoint x y) (a : ℝ) : IsVLDisjoint x (a • y)

Scalar multiplication on the right preserves disjointness.

theorem exists_pair_ne_zero_isVLDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] [IsVLArchimedean X] (h : 1 < Module.rank ℝ X) : ∃ (u : X) (v : X), u ≠ 0 ∧ v ≠ 0 ∧ IsVLDisjoint u v

Two non-zero disjoint vectors exist in any Archimedean vector lattice of ℝ-rank greater than one.

Disjoint positive parts from scalar multiples

theorem isVLDisjoint_posPart_sub_smul {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (x y : X) {lam : ℝ} (hlam : 0 < lam) : IsVLDisjoint (x - lam • y)⁺ (y - lam⁻¹ • x)⁺

For any x, y and λ > 0, the positive parts (x - λ • y)⁺ and (y - λ⁻¹ • x)⁺ are disjoint.

Finite disjoint families with scalars

theorem abs_sum_finset {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {ι : Type u_2} (s : Finset ι) (x : ι → X) (α : ι → ℝ) (hdisj : (↑s).Pairwise fun (i j : ι) => IsVLDisjoint (x i) (x j)) : |∑ i ∈ s, α i • x i| = ∑ i ∈ s, |α i| • |x i|

Absolute value distributes over a scaled finite disjoint family.

theorem abs_sum_of_pairwise_isVLDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {n : ℕ} {x : Fin n → X} {α : Fin n → ℝ} (hdisj : Pairwise fun (i j : Fin n) => IsVLDisjoint (x i) (x j)) : |∑ i : Fin n, α i • x i| = ∑ i : Fin n, |α i| • |x i|

For a pairwise-disjoint family and arbitrary scalars, |∑ i, α i • x i| = ∑ i, |α i| • |x i|.

theorem sup_smul_eq_sum_of_pairwise_isVLDisjoint_of_nonneg {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {n : ℕ} {x : Fin n → X} {α : Fin n → ℝ} (hne : 0 < n) (hnn : ∀ (i : Fin n), 0 ≤ x i) (hα : ∀ (i : Fin n), 0 ≤ α i) (hdisj : Pairwise fun (i j : Fin n) => IsVLDisjoint (x i) (x j)) : ∑ i : Fin n, α i • x i = Finset.univ.sup' ⋯ fun (i : Fin n) => α i • x i

For a pairwise-disjoint family of non-negative elements and non-negative scalars, ∑ i, α i • x i = ⨆ i, α i • x i (with the sup taken over a non-empty index).

theorem linearIndependent_of_pairwise_isVLDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {n : ℕ} {x : Fin n → X} (hne : ∀ (i : Fin n), x i ≠ 0) (hdisj : Pairwise fun (i j : Fin n) => IsVLDisjoint (x i) (x j)) : LinearIndependent ℝ x

A pairwise-disjoint family of non-zero vectors is linearly independent over ℝ.

Pairwise disjoint families and maximality

A subset of a vector lattice is pairwise disjoint when distinct members are vector-lattice disjoint, and maximal when it is not properly contained in any strictly larger pairwise disjoint subset. Every vector lattice admits a maximal disjoint family consisting of strictly positive vectors, by Zorn's lemma.

def IsDisjointSet {X : Type u_1} [AddCommGroup X] [Lattice X] (Λ : Set X) : Prop

A subset of X is pairwise disjoint when it does not contain 0 and distinct members are vector-lattice disjoint.

Equations

• IsDisjointSet Λ = (0 ∉ Λ ∧ ∀ ⦃a : X⦄, a ∈ Λ → ∀ ⦃b : X⦄, b ∈ Λ → a ≠ b → IsVLDisjoint a b)

def IsMaximalDisjoint {X : Type u_1} [AddCommGroup X] [Lattice X] (Λ : Set X) : Prop

A maximal disjoint family in X is a pairwise disjoint set that is not properly contained in any strictly larger pairwise disjoint subset of X. The order is by inclusion (not refinement).

Equations

• IsMaximalDisjoint Λ = Maximal IsDisjointSet Λ

theorem isMaximalDisjoint_iff_forall_eq_zero {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {Λ : Set X} (hdis : IsDisjointSet Λ) : IsMaximalDisjoint Λ ↔ ∀ (x : X), (∀ a ∈ Λ, IsVLDisjoint x a) → x = 0

A pairwise disjoint family of nonzero elements is maximal iff the only element disjoint from every member of the family is 0.

theorem exists_isMaximalDisjoint_pos (X : Type u_2) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] : ∃ (Λ : Set X), IsMaximalDisjoint Λ ∧ ∀ x ∈ Λ, 0 < x

Existence of a maximal disjoint family of positive vectors. Every vector lattice admits a maximal disjoint family whose elements are all strictly positive.

Disjoint sequences in normed vector lattices

theorem eq_zero_of_pairwise_isVLDisjoint_tendsto {Y : Type u_1} [NormedAddCommGroup Y] [Lattice Y] [IsOrderedAddMonoid Y] [NormedVectorLattice Y] {u : ℕ → Y} {x : Y} (hdisj : Pairwise fun (i j : ℕ) => IsVLDisjoint (u i) (u j)) (hlim : Filter.Tendsto u Filter.atTop (nhds x)) : x = 0

In a normed vector lattice, a limit of a pairwise-disjoint sequence is zero.