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 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 : ℝ) : IsSolid (Metric.ball 0 r)

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

instance instHasSolidNormReal : HasSolidNorm ℝ

instance instHasSolidNormRat : HasSolidNorm ℚ

class NormedLatticeAddCommGroup (α : Type u_1) extends NormedAddCommGroup α, Lattice α, HasSolidNorm α : 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.

• norm : α → ℝ
• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• add_comm (a b : α) : a + b = b + a
• dist : α → α → ℝ
• dist_self (x : α) : dist x x = 0
• dist_comm (x y : α) : dist x y = dist y x
• dist_triangle (x y z : α) : dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist (x y : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y
• dist_eq (x y : α) : dist x y = ‖x - y‖
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• solid ⦃x y : α⦄ : |x| ≤ |y| → ‖x‖ ≤ ‖y‖
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b

instance Int.normedLatticeAddCommGroup : NormedLatticeAddCommGroup ℤ

Equations

• Int.normedLatticeAddCommGroup = NormedLatticeAddCommGroup.mk Int.normedLatticeAddCommGroup.proof_2

instance Rat.normedLatticeAddCommGroup : NormedLatticeAddCommGroup ℚ

Equations

• Rat.normedLatticeAddCommGroup = NormedLatticeAddCommGroup.mk Rat.normedLatticeAddCommGroup.proof_2

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.

@[instance 100]

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

@[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.

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