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

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

instance instHasSolidNormRealNormedAddCommGroupLattice : HasSolidNorm ℝ

Equations

• instHasSolidNormRealNormedAddCommGroupLattice = (_ : HasSolidNorm ℝ)

instance instHasSolidNormRatNormedAddCommGroupInstLatticeRat : HasSolidNorm ℚ

Equations

• instHasSolidNormRatNormedAddCommGroupInstLatticeRat = (_ : 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 = x + AddMonoid.nsmul n 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 (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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 : α), PseudoMetricSpace.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‖
• sup : α → α → α
• 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
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
• solid : ∀ ⦃x y : α⦄, |x| ≤ |y| → ‖x‖ ≤ ‖y‖
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

instance Real.normedLatticeAddCommGroup : NormedLatticeAddCommGroup ℝ

Equations

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

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 (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b)

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

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

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 : α) : ‖|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 NormedLatticeAddCommGroup.continuousInf {α : Type u_1} [NormedLatticeAddCommGroup α] : ContinuousInf α

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

Equations

• (_ : ContinuousInf α) = (_ : ContinuousInf α)

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

Equations

• (_ : ContinuousSup α) = (_ : ContinuousSup αᵒᵈᵒᵈ)

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

• (_ : TopologicalLattice α) = (_ : TopologicalLattice α)

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 NormedLatticeAddCommGroup.orderClosedTopology {E : Type u_2} [NormedLatticeAddCommGroup E] : OrderClosedTopology E

Equations

• (_ : OrderClosedTopology E) = (_ : OrderClosedTopology E)