Documentation

Mathlib.Analysis.Normed.Order.Lattice

Normed lattice ordered groups #

Motivated by the theory of Banach Lattices, we then define NormedLatticeAddCommGroup as a lattice with a covariant normed group addition satisfying the solid axiom.

Main statements #

We show that a normed lattice ordered group is a topological lattice with respect to the norm topology.

References #

Tags #

normed, lattice, ordered, group

Normed lattice ordered groups #

Motivated by the theory of Banach Lattices, this section introduces normed lattice ordered groups.

source
class HasSolidNorm (α : Type u_1) [NormedAddCommGroup α] [Lattice α] :
Prop

Let α be an AddCommGroup with a Lattice structure. A norm on α is solid if, for a and b in α, with absolute values |a| and |b| respectively, |a| ≤ |b| implies ‖a‖ ≤ ‖b‖.

Instances
    source
    theorem norm_le_norm_of_abs_le_abs {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] {a b : α} (h : |a| ≤ |b|) :
    ‖a‖ ≤ ‖b‖
    source
    theorem LatticeOrderedAddCommGroup.isSolid_ball {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] (r : ℝ) :
    IsSolid (Metric.ball 0 r)

    If α has a solid norm, then the balls centered at the origin of α are solid sets.

    source
    instance instHasSolidNormReal :
    HasSolidNorm ℝ
    source
    instance instHasSolidNormRat :
    HasSolidNorm ℚ
    source
    instance Int.hasSolidNorm :
    HasSolidNorm ℤ
    source
    theorem dual_solid {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (a b : α) (h : b ⊓ -b ≤ a ⊓ -a) :
    ‖a‖ ≤ ‖b‖
    source
    @[instance 100]
    instance OrderDual.instHasSolidNorm {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] :
    HasSolidNorm αᵒᵈ

    Let α be a normed lattice ordered group, then the order dual is also a normed lattice ordered group.

    source
    theorem norm_abs_eq_norm {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (a : α) :
    ‖|a|‖ = ‖a‖
    source
    theorem norm_inf_sub_inf_le_add_norm {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (a b c d : α) :
    ‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖
    source
    theorem norm_sup_sub_sup_le_add_norm {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (a b c d : α) :
    ‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖
    source
    theorem norm_inf_le_add {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (x y : α) :
    ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
    source
    theorem norm_sup_le_add {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (x y : α) :
    ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
    source
    @[instance 100]
    instance HasSolidNorm.continuousInf {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] :
    ContinuousInf α

    Let α be a normed lattice ordered group. Then the infimum is jointly continuous.

    source
    @[instance 100]
    instance HasSolidNorm.continuousSup {α : Type u_2} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] :
    ContinuousSup α
    source
    @[instance 100]
    instance HasSolidNorm.toTopologicalLattice {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] :
    TopologicalLattice α

    Let α be a normed lattice ordered group. Then α is a topological lattice in the norm topology.

    source
    theorem norm_abs_sub_abs {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (a b : α) :
    ‖|a| - |b|‖ ≤ ‖a - b‖
    source
    theorem norm_sup_sub_sup_le_norm {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (x y z : α) :
    ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
    source
    theorem norm_inf_sub_inf_le_norm {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (x y z : α) :
    ‖x ⊓ z - y ⊓ z‖ ≤ ‖x - y‖
    source
    theorem lipschitzWith_sup_right {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (z : α) :
    LipschitzWith 1 fun (x : α) => x ⊔ z
    source
    theorem lipschitzWith_posPart {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] :
    LipschitzWith 1 posPart
    source
    theorem lipschitzWith_negPart {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] :
    LipschitzWith 1 negPart
    source
    theorem continuous_posPart {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] :
    Continuous posPart
    source
    theorem continuous_negPart {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] :
    Continuous negPart
    source
    theorem isClosed_nonneg {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] :
    IsClosed {x : α | 0 ≤ x}
    source
    theorem isClosed_le_of_isClosed_nonneg {G : Type u_2} [AddCommGroup G] [PartialOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [ContinuousSub G] (h : IsClosed {x : G | 0 ≤ x}) :
    IsClosed {p : G × G | p.1 ≤ p.2}
    source
    @[instance 100]
    instance HasSolidNorm.orderClosedTopology {E : Type u_2} [NormedAddCommGroup E] [Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] :
    OrderClosedTopology E