Meyer-Nieberg theorem

A Banach lattice has an order continuous norm iff every order-bounded pairwise disjoint sequence converges to zero in norm. As a corollary, in an order continuous Banach lattice every order-bounded set of pairwise disjoint non-zero elements is at most countable.

theorem exists_disjoint_sequences_approx_of_monotone_le {E : Type u_2} [AddCommGroup E] [Lattice E] [IsOrderedAddMonoid E] [VectorLattice E] {x : E} {u : ℕ → E} (h0 : ∀ (n : ℕ), 0 ≤ u n) (hmono : Monotone u) (hle : ∀ (n : ℕ), u n ≤ x) {k : ℕ} (hk : 0 < k) : ∃ (y : Fin k → ℕ → E), (∀ (i : Fin k), Pairwise fun (n m : ℕ) => IsVLDisjoint (y i n) (y i m)) ∧ (∀ (i : Fin k) (n : ℕ), y i n ∈ Set.Icc 0 x) ∧ ∀ (n : ℕ), ∑ i : Fin k, y i n ≤ u (n + 1) - u n ∧ u (n + 1) - u n ≤ ∑ i : Fin k, y i n + (2 / (↑k + 3)) • x

Disjointification of increments of an increasing order-bounded sequence.

theorem monotone_le_cauchySeq_iff_disjoint_tendsto_zero {E : Type u_2} [NormedAddCommGroup E] [Lattice E] [IsOrderedAddMonoid E] [NormedVectorLattice E] {x : E} (hx : 0 ≤ x) : (∀ {u : ℕ → E}, (∀ (n : ℕ), 0 ≤ u n) → Monotone u → (∀ (n : ℕ), u n ≤ x) → CauchySeq u) ↔ ∀ {u : ℕ → E}, (∀ (n : ℕ), u n ∈ Set.Icc 0 x) → (Pairwise fun (n m : ℕ) => IsVLDisjoint (u n) (u m)) → Filter.Tendsto u Filter.atTop (nhds 0)

For a normed vector lattice, increasing sequences bounded by x are norm-Cauchy iff disjoint sequences in [0, x] converge to zero in norm.

theorem BanachLattice.disjoint_bddAbove_tendsto_zero {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] [IsOrderContinuousNorm X] {u : ℕ → X} (hd : Pairwise fun (i j : ℕ) => IsVLDisjoint (u i) (u j)) (hbd : BddAbove (Set.range fun (n : ℕ) => |u n|)) : Filter.Tendsto u Filter.atTop (nhds 0)

In an order continuous Banach lattice, every order-bounded pairwise disjoint sequence converges to zero in norm.

theorem BanachLattice.isOrderContinuousNorm_of_disjoint_tendsto_zero {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] (h : ∀ {u : ℕ → X}, (Pairwise fun (i j : ℕ) => IsVLDisjoint (u i) (u j)) → BddAbove (Set.range fun (n : ℕ) => |u n|) → Filter.Tendsto u Filter.atTop (nhds 0)) : IsOrderContinuousNorm X

A Banach lattice whose order-bounded pairwise disjoint sequences all converge to zero in norm has an order continuous norm.

theorem BanachLattice.isOrderContinuousNorm_iff_disjoint_tendsto_zero {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] : IsOrderContinuousNorm X ↔ ∀ {u : ℕ → X}, (Pairwise fun (i j : ℕ) => IsVLDisjoint (u i) (u j)) → BddAbove (Set.range fun (n : ℕ) => |u n|) → Filter.Tendsto u Filter.atTop (nhds 0)

Meyer-Nieberg theorem: a Banach lattice has an order continuous norm iff every order-bounded pairwise disjoint sequence converges to zero.

theorem BanachLattice.countable_of_pairwise_disjoint_bddAbove {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] [IsOrderContinuousNorm X] {S : Set X} (h0 : ∀ x ∈ S, x ≠ 0) (hd : S.Pairwise fun (x y : X) => IsVLDisjoint x y) (hbd : BddAbove ((fun (x : X) => |x|) '' S)) : S.Countable

In an order continuous Banach lattice, any order-bounded set of pairwise disjoint non-zero elements is at most countable.