Normed vector lattices and Banach lattices

A normed vector lattice is a real vector lattice whose norm satisfies the solid axiom: |x| ≤ |y| implies ‖x‖ ≤ ‖y‖. This single condition encodes compatibility between the norm and the lattice structure. A Banach lattice is a normed vector lattice whose norm is complete. This file develops the basic topology of normed vector lattices, including continuity of lattice operations, closedness of the positive cone, boundedness of order intervals, and monotone convergence facts.

class NormedVectorLattice (X : Type u_1) [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] extends VectorLattice X, HasSolidNorm X, NormSMulClass ℝ X : Type u_1

A normed vector lattice is a real vector lattice equipped with a lattice norm: a norm satisfying |x| ≤ |y| → ‖x‖ ≤ ‖y‖.

• smul : ℝ → X → X
• mul_smul (x y : ℝ) (b : X) : (x * y) • b = x • y • b
• one_smul (b : X) : 1 • b = b
• smul_zero (a : ℝ) : a • 0 = 0
• smul_add (a : ℝ) (x y : X) : a • (x + y) = a • x + a • y
• add_smul (r s : ℝ) (x : X) : (r + s) • x = r • x + s • x
• zero_smul (x : X) : 0 • x = 0
• smul_le_smul_of_nonneg_left ⦃a : ℝ⦄ (ha : 0 ≤ a) ⦃b₁ b₂ : X⦄ (hb : b₁ ≤ b₂) : a • b₁ ≤ a • b₂
• solid ⦃x y : X⦄ : |x| ≤ |y| → ‖x‖ ≤ ‖y‖
• norm_smul (r : ℝ) (x : X) : ‖r • x‖ = ‖r‖ * ‖x‖

@[instance_reducible]

instance NormedVectorLattice.instNormedSpace {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : NormedSpace ℝ X

A normed vector lattice is a normed space over ℝ.

Equations

• NormedVectorLattice.instNormedSpace = { toModule := inst✝.toModule, norm_smul_le := ⋯ }

Continuity of lattice operations

theorem NormedVectorLattice.continuous_sup {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : Continuous fun (p : X × X) => p.1 ⊔ p.2

Supremum is jointly norm-continuous.

theorem NormedVectorLattice.continuous_inf {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : Continuous fun (p : X × X) => p.1 ⊓ p.2

Infimum is jointly norm-continuous.

theorem NormedVectorLattice.lipschitzWith_abs {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : LipschitzWith 1 fun (x : X) => |x|

The absolute value map is Lipschitz with constant 1; in particular it is continuous.

theorem NormedVectorLattice.norm_posPart_le {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (x : X) : ‖x⁺‖ ≤ ‖x‖

The norm of the positive part is bounded by the norm.

Archimedean property

instance NormedVectorLattice.instIsVLArchimedean {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : IsVLArchimedean X

Every normed vector lattice is Archimedean in the vector-lattice sense: the only non-negative element all of whose multiples are bounded is zero.

Closed positive cone and order topology

instance NormedVectorLattice.instOrderClosedTopology {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : OrderClosedTopology X

The order relation is closed in a normed vector lattice.

theorem NormedVectorLattice.isClosed_nonneg_cone {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : IsClosed {x : X | 0 ≤ x}

The positive cone {x | 0 ≤ x} is norm-closed.

theorem NormedVectorLattice.le_of_tendsto_of_tendsto {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] {u v : ℕ → X} {a b : X} (hu : Filter.Tendsto u Filter.atTop (nhds a)) (hv : Filter.Tendsto v Filter.atTop (nhds b)) (h : ∀ (n : ℕ), u n ≤ v n) : a ≤ b

Inequalities are preserved under norm limits: if u n ≤ v n for all n, and u n → a, v n → b in norm, then a ≤ b.

Monotone Convergence Lemma

theorem NormedVectorLattice.isLUB_of_monotone_tendsto {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] {u : ℕ → X} {l : X} (hmono : Monotone u) (hlim : Filter.Tendsto u Filter.atTop (nhds l)) : IsLUB (Set.range u) l

Monotone Convergence Lemma: an increasing sequence converging in norm is a least upper bound for its range.

theorem NormedVectorLattice.isGLB_of_antitone_tendsto {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] {u : ℕ → X} {l : X} (hanti : Antitone u) (hlim : Filter.Tendsto u Filter.atTop (nhds l)) : IsGLB (Set.range u) l

Antitone Convergence Lemma: a decreasing sequence converging in norm is a greatest lower bound for its range.

Closed and bounded intervals

theorem NormedVectorLattice.isClosed_interval {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (a b : X) : IsClosed (Set.Icc a b)

Order intervals are norm-closed.

theorem NormedVectorLattice.norm_le_norm_abs_sup_abs_of_mem_Icc {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] {a b x : X} (hx : x ∈ Set.Icc a b) : ‖x‖ ≤ ‖|a| ⊔ |b|‖

Every element x ∈ [a, b] satisfies ‖x‖ ≤ ‖|a| ⊔ |b|‖. In particular, every order interval is norm-bounded.

theorem NormedVectorLattice.isBounded_of_bddBelow_bddAbove {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] {s : Set X} (hl : BddBelow s) (hu : BddAbove s) : Bornology.IsBounded s

Order-bounded sets are norm-bounded.

Banach lattices

class BanachLattice (X : Type u_1) [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] extends NormedVectorLattice X, CompleteSpace X : Type u_1

A Banach lattice is a normed vector lattice with a complete norm.

• smul : ℝ → X → X
• mul_smul (x y : ℝ) (b : X) : (x * y) • b = x • y • b
• one_smul (b : X) : 1 • b = b
• smul_zero (a : ℝ) : a • 0 = 0
• smul_add (a : ℝ) (x y : X) : a • (x + y) = a • x + a • y
• add_smul (r s : ℝ) (x : X) : (r + s) • x = r • x + s • x
• zero_smul (x : X) : 0 • x = 0
• smul_le_smul_of_nonneg_left ⦃a : ℝ⦄ (ha : 0 ≤ a) ⦃b₁ b₂ : X⦄ (hb : b₁ ≤ b₂) : a • b₁ ≤ a • b₂
• solid ⦃x y : X⦄ : |x| ≤ |y| → ‖x‖ ≤ ‖y‖
• norm_smul (r : ℝ) (x : X) : ‖r • x‖ = ‖r‖ * ‖x‖
• complete {f : Filter X} : Cauchy f → ∃ (x : X), f ≤ nhds x

@[instance_reducible]

noncomputable instance instNormedVectorLatticeReal : NormedVectorLattice ℝ

The real numbers form a normed vector lattice over themselves.

Equations

• instNormedVectorLatticeReal = { toVectorLattice := instVectorLatticeReal, toHasSolidNorm := instHasSolidNormReal, toNormSMulClass := instNormedVectorLatticeReal._proof_1 }

@[instance_reducible]

noncomputable instance instBanachLatticeReal : BanachLattice ℝ

The real numbers form a Banach lattice over themselves.

Equations

• instBanachLatticeReal = { toNormedVectorLattice := instNormedVectorLatticeReal, toCompleteSpace := Real.instCompleteSpace }

Completion of a normed vector lattice

The metric completion of a normed vector lattice carries a compatible lattice structure making it again a normed vector lattice; being complete, it is a Banach lattice.

@[instance_reducible]

noncomputable instance instLatticeCompletion {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : Lattice (UniformSpace.Completion X)

The completion of a normed vector lattice is a lattice.

Equations

• instLatticeCompletion = Lattice.mk' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem coe_sup_completion {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (x y : X) : ↑(x ⊔ y) = ↑x ⊔ ↑y

The inclusion of a normed vector lattice into its completion preserves suprema.

theorem coe_inf_completion {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (x y : X) : ↑(x ⊓ y) = ↑x ⊓ ↑y

The inclusion of a normed vector lattice into its completion preserves infima.

theorem coe_abs_completion {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] (x : X) : ↑|x| = |↑x|

The inclusion of a normed vector lattice into its completion preserves absolute values.

instance instIsOrderedAddMonoidCompletion {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : IsOrderedAddMonoid (UniformSpace.Completion X)

The order on the completion of a normed vector lattice is compatible with addition.

@[instance_reducible]

noncomputable instance instVectorLatticeCompletion {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : VectorLattice (UniformSpace.Completion X)

Equations

• instVectorLatticeCompletion = { toModule := UniformSpace.Completion.instModule, toPosSMulMono := ⋯ }

instance instHasSolidNormCompletion {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : HasSolidNorm (UniformSpace.Completion X)

The completion of a normed vector lattice has a solid norm.

@[instance_reducible]

noncomputable instance instNormedVectorLatticeCompletion {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : NormedVectorLattice (UniformSpace.Completion X)

The completion of a normed vector lattice is a normed vector lattice.

Equations

• instNormedVectorLatticeCompletion = { toVectorLattice := instVectorLatticeCompletion, toHasSolidNorm := ⋯, toNormSMulClass := ⋯ }

@[instance_reducible]

noncomputable instance instBanachLatticeCompletion {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : BanachLattice (UniformSpace.Completion X)

The completion of a normed vector lattice is a Banach lattice.

Equations

• instBanachLatticeCompletion = { toNormedVectorLattice := instNormedVectorLatticeCompletion, toCompleteSpace := ⋯ }

theorem isometry_coe_completion {X : Type u_1} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] : Isometry UniformSpace.Completion.coe'

The canonical inclusion into the completion preserves the isometry to toComplₗᵢ; it is an isometry from X into its completion.