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

• [Meyer-Nieberg, Banach lattices][MeyerNieberg1991]

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 α] : 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‖.

• solid : ∀ ⦃x y : α⦄, |x| ≤ |y| → ‖x‖ ≤ ‖y‖

theorem HasSolidNorm.solid {α : Type u_1} : ∀ {inst : NormedAddCommGroup α} {inst_1 : 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|) : ‖a‖ ≤ ‖b‖

theorem LatticeOrderedAddCommGroup.isSolid_ball {α : Type u_1} [NormedAddCommGroup α] [Lattice α] [HasSolidNorm α] (r : ℝ) : LatticeOrderedAddCommGroup.IsSolid (Metric.ball 0 r)

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

instance instHasSolidNormReal : HasSolidNorm ℝ

Equations

• instHasSolidNormReal = ⋯

instance instHasSolidNormRat : HasSolidNorm ℚ

Equations

• instHasSolidNormRat = ⋯

class NormedLatticeAddCommGroup (α : Type u_1) extends NormedAddCommGroup , Lattice , HasSolidNorm , Norm , AddCommGroup , MetricSpace , AddGroup , AddCommMonoid , SubNegMonoid , AddMonoid , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , PseudoMetricSpace , Dist , SemilatticeSup , SemilatticeInf , Sup , Inf , PartialOrder , Preorder , LE , LT : Type u_1

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.

theorem NormedLatticeAddCommGroup.add_le_add_left {α : Type u_1} [self : NormedLatticeAddCommGroup α] (a : α) (b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b

instance Real.normedLatticeAddCommGroup : NormedLatticeAddCommGroup ℝ

Equations

• Real.normedLatticeAddCommGroup = NormedLatticeAddCommGroup.mk Real.normedLatticeAddCommGroup.proof_1

@[instance 100]

instance NormedLatticeAddCommGroup.toOrderedAddCommGroup {α : Type u_1} [h : NormedLatticeAddCommGroup α] : OrderedAddCommGroup α

A normed lattice ordered group is an ordered additive commutative group

Equations

• NormedLatticeAddCommGroup.toOrderedAddCommGroup = OrderedAddCommGroup.mk ⋯

theorem dual_solid {α : Type u_1} [NormedLatticeAddCommGroup α] (a : α) (b : α) (h : b ⊓ -b ≤ a ⊓ -a) : ‖a‖ ≤ ‖b‖

@[instance 100]

instance OrderDual.instNormedLatticeAddCommGroup {α : Type u_1} [NormedLatticeAddCommGroup α] : NormedLatticeAddCommGroup αᵒᵈ

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

Equations

• OrderDual.instNormedLatticeAddCommGroup = NormedLatticeAddCommGroup.mk ⋯

theorem norm_abs_eq_norm {α : Type u_1} [NormedLatticeAddCommGroup α] (a : α) : ‖|a|‖ = ‖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 : α) : ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖

theorem norm_sup_le_add {α : Type u_1} [NormedLatticeAddCommGroup α] (x : α) (y : α) : ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖

@[instance 100]

instance NormedLatticeAddCommGroup.continuousInf {α : Type u_1} [NormedLatticeAddCommGroup α] : ContinuousInf α

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

Equations

• ⋯ = ⋯

@[instance 100]

instance NormedLatticeAddCommGroup.continuousSup {α : Type u_2} [NormedLatticeAddCommGroup α] : ContinuousSup α

Equations

• ⋯ = ⋯

@[instance 100]

instance NormedLatticeAddCommGroup.toTopologicalLattice {α : Type u_1} [NormedLatticeAddCommGroup α] : TopologicalLattice α

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 lipschitzWith_posPart {α : Type u_1} [NormedLatticeAddCommGroup α] : LipschitzWith 1 posPart

theorem lipschitzWith_negPart {α : Type u_1} [NormedLatticeAddCommGroup α] : LipschitzWith 1 negPart

theorem continuous_posPart {α : Type u_1} [NormedLatticeAddCommGroup α] : Continuous posPart

theorem continuous_negPart {α : Type u_1} [NormedLatticeAddCommGroup α] : Continuous negPart

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}

@[instance 100]

instance NormedLatticeAddCommGroup.orderClosedTopology {E : Type u_2} [NormedLatticeAddCommGroup E] : OrderClosedTopology E

Equations

• ⋯ = ⋯