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.

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

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
    theorem HasSolidNorm.solid {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [self : HasSolidNorm α] ⦃x : α ⦃y : α :
    |x| |y|x y
    theorem norm_le_norm_of_abs_le_abs {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] {a : α} {b : α} (h : |a| |b|) :

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

    Let α be a normed commutative group equipped with a partial order covariant with addition, with respect which α forms a lattice. Suppose that α is solid, that is to say, for a and b in α, with absolute values |a| and |b| respectively, |a| ≤ |b| implies ‖a‖ ≤ ‖b‖. Then α is said to be a normed lattice ordered group.

    Instances
      theorem NormedLatticeAddCommGroup.add_le_add_left {α : Type u_1} [self : NormedLatticeAddCommGroup α] (a : α) (b : α) :
      a b∀ (c : α), c + a c + b
      @[instance 100]

      A normed lattice ordered group is an ordered additive commutative group

      Equations
      theorem dual_solid {α : Type u_1} [NormedLatticeAddCommGroup α] (a : α) (b : α) (h : b -b a -a) :
      @[instance 100]

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

      Equations
      • One or more equations did not get rendered due to their size.
      theorem norm_abs_eq_norm {α : Type u_1} [NormedLatticeAddCommGroup α] (a : α) :
      theorem norm_inf_sub_inf_le_add_norm {α : Type u_1} [NormedLatticeAddCommGroup α] (a : α) (b : α) (c : α) (d : α) :
      a b - c d a - c + b - d
      theorem norm_sup_sub_sup_le_add_norm {α : Type u_1} [NormedLatticeAddCommGroup α] (a : α) (b : α) (c : α) (d : α) :
      a b - c d a - c + b - d
      theorem norm_inf_le_add {α : Type u_1} [NormedLatticeAddCommGroup α] (x : α) (y : α) :
      theorem norm_sup_le_add {α : Type u_1} [NormedLatticeAddCommGroup α] (x : α) (y : α) :
      @[instance 100]

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

      Equations
      • =
      @[instance 100]
      Equations
      • =
      @[instance 100]

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

      Equations
      • =
      theorem norm_abs_sub_abs {α : Type u_1} [NormedLatticeAddCommGroup α] (a : α) (b : α) :
      |a| - |b| a - b
      theorem norm_sup_sub_sup_le_norm {α : Type u_1} [NormedLatticeAddCommGroup α] (x : α) (y : α) (z : α) :
      x z - y z x - y
      theorem norm_inf_sub_inf_le_norm {α : Type u_1} [NormedLatticeAddCommGroup α] (x : α) (y : α) (z : α) :
      x z - y z x - y
      theorem lipschitzWith_sup_right {α : Type u_1} [NormedLatticeAddCommGroup α] (z : α) :
      LipschitzWith 1 fun (x : α) => x z
      theorem isClosed_nonneg {α : Type u_1} [NormedLatticeAddCommGroup α] :
      IsClosed {x : α | 0 x}
      theorem isClosed_le_of_isClosed_nonneg {G : Type u_2} [OrderedAddCommGroup G] [TopologicalSpace G] [ContinuousSub G] (h : IsClosed {x : G | 0 x}) :
      IsClosed {p : G × G | p.1 p.2}