Nakano's theorem

For a Banach lattice the following are equivalent:

• the norm is order continuous;
• the lattice is σ-conditionally complete and the norm is σ-order continuous;
• every increasing order-bounded sequence converges in norm.

The equivalence is recorded through the corresponding implications between order continuity, σ-conditional completeness, σ-order continuity, and monotone norm convergence of bounded sequences.

theorem BanachLattice.tendsto_of_monotone_bddAbove {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] [IsOrderContinuousNorm X] {u : ℕ → X} (hmono : Monotone u) (hbd : BddAbove (Set.range u)) : ∃ (x : X), IsLUB (Set.range u) x ∧ Filter.Tendsto u Filter.atTop (nhds x)

In an order continuous Banach lattice, every increasing order-bounded sequence converges in norm to its supremum.

@[reducible]

noncomputable def BanachLattice.sigmaConditionallyCompleteLatticeOfMonoBddAboveTendsto {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (h : ∀ {u : ℕ → X}, Monotone u → BddAbove (Set.range u) → ∃ (x : X), IsLUB (Set.range u) x ∧ Filter.Tendsto u Filter.atTop (nhds x)) : SigmaConditionallyCompleteLattice X

A lattice-ordered additive commutative group in which every increasing order-bounded sequence converges in norm to a least upper bound is σ-conditionally complete.

Equations

• BanachLattice.sigmaConditionallyCompleteLatticeOfMonoBddAboveTendsto h = sigmaConditionallyCompleteLatticeOfPosSeq X ⋯

theorem BanachLattice.isSigmaOrderContinuousNorm_of_mono_bddAbove_tendsto {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [BanachLattice X] (h : ∀ {u : ℕ → X}, Monotone u → BddAbove (Set.range u) → ∃ (x : X), IsLUB (Set.range u) x ∧ Filter.Tendsto u Filter.atTop (nhds x)) : IsSigmaOrderContinuousNorm X

A Banach lattice in which every increasing order-bounded sequence converges in norm has a σ-order continuous norm.

theorem BanachLattice.isOrderContinuousNorm_of_isSigmaConditionallyCompleteLattice {X : Type u_1} [NormedAddCommGroup X] [SigmaConditionallyCompleteLattice X] [IsOrderedAddMonoid X] [BanachLattice X] [IsSigmaOrderContinuousNorm X] : IsOrderContinuousNorm X

A Banach lattice that is σ-conditionally complete and has σ-order continuous norm has an order continuous norm.