mathlib3 documentation

analysis.normed.order.lattice

Normed lattice ordered groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Motivated by the theory of Banach Lattices, we then define normed_lattice_add_comm_group 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]
structure has_solid_norm (α : Type u_1) [normed_add_comm_group α] [lattice α] :
Prop

Let α be an add_comm_group 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 of this typeclass
source
theorem norm_le_norm_of_abs_le_abs {α : Type u_1} [normed_add_comm_group α] [lattice α] [has_solid_norm α] {a b : α} (h : |a| ≤ |b|) :
‖a‖ ≤ ‖b‖
source
theorem lattice_ordered_add_comm_group.is_solid_ball {α : Type u_1} [normed_add_comm_group α] [lattice α] [has_solid_norm α] (r : ℝ) :
lattice_ordered_add_comm_group.is_solid (metric.ball 0 r)

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

source
@[protected, instance]
def real.has_solid_norm  :
has_solid_norm ℝ
source
@[protected, instance]
def rat.has_solid_norm  :
has_solid_norm ℚ
source
@[class]
structure normed_lattice_add_comm_group (α : Type u_1) :
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.

Instances of this typeclass
Instances of other typeclasses for normed_lattice_add_comm_group
  • normed_lattice_add_comm_group.has_sizeof_inst
source
@[protected, instance]
def real.normed_lattice_add_comm_group  :
normed_lattice_add_comm_group ℝ
Equations
source
@[protected, instance]
def normed_lattice_add_comm_group_to_ordered_add_comm_group {α : Type u_1} [h : normed_lattice_add_comm_group α] :
ordered_add_comm_group α

A normed lattice ordered group is an ordered additive commutative group

Equations
source
theorem dual_solid {α : Type u_1} [normed_lattice_add_comm_group α] (a b : α) (h : b ⊓ -b ≤ a ⊓ -a) :
‖a‖ ≤ ‖b‖
source
@[protected, instance]
def order_dual.normed_lattice_add_comm_group {α : Type u_1} [normed_lattice_add_comm_group α] :
normed_lattice_add_comm_group αᵒᵈ

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

Equations
source
theorem norm_abs_eq_norm {α : Type u_1} [normed_lattice_add_comm_group α] (a : α) :
‖|a|‖ = ‖a‖
source
theorem norm_inf_sub_inf_le_add_norm {α : Type u_1} [normed_lattice_add_comm_group α] (a b c d : α) :
‖a ⊓ b - c ⊓ d‖ ≤ ‖a - c‖ + ‖b - d‖
source
theorem norm_sup_sub_sup_le_add_norm {α : Type u_1} [normed_lattice_add_comm_group α] (a b c d : α) :
‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖
source
theorem norm_inf_le_add {α : Type u_1} [normed_lattice_add_comm_group α] (x y : α) :
‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
source
theorem norm_sup_le_add {α : Type u_1} [normed_lattice_add_comm_group α] (x y : α) :
‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
source
@[protected, instance]
def normed_lattice_add_comm_group_has_continuous_inf {α : Type u_1} [normed_lattice_add_comm_group α] :
has_continuous_inf α

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

source
@[protected, instance]
def normed_lattice_add_comm_group_has_continuous_sup {α : Type u_1} [normed_lattice_add_comm_group α] :
has_continuous_sup α
source
@[protected, instance]
def normed_lattice_add_comm_group_topological_lattice {α : Type u_1} [normed_lattice_add_comm_group α] :
topological_lattice α

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

Equations
source
theorem norm_abs_sub_abs {α : Type u_1} [normed_lattice_add_comm_group α] (a b : α) :
‖|a| - |b|‖ ≤ ‖a - b‖
source
theorem norm_sup_sub_sup_le_norm {α : Type u_1} [normed_lattice_add_comm_group α] (x y z : α) :
‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
source
theorem norm_inf_sub_inf_le_norm {α : Type u_1} [normed_lattice_add_comm_group α] (x y z : α) :
‖x ⊓ z - y ⊓ z‖ ≤ ‖x - y‖
source
theorem lipschitz_with_sup_right {α : Type u_1} [normed_lattice_add_comm_group α] (z : α) :
lipschitz_with 1 (λ (x : α), x ⊔ z)
source
theorem lipschitz_with_pos {α : Type u_1} [normed_lattice_add_comm_group α] :
lipschitz_with 1 has_pos_part.pos
source
theorem continuous_pos {α : Type u_1} [normed_lattice_add_comm_group α] :
continuous has_pos_part.pos
source
theorem continuous_neg' {α : Type u_1} [normed_lattice_add_comm_group α] :
continuous has_neg_part.neg
source
theorem is_closed_nonneg {E : Type u_1} [normed_lattice_add_comm_group E] :
is_closed {x : E | 0 ≤ x}
source
theorem is_closed_le_of_is_closed_nonneg {G : Type u_1} [ordered_add_comm_group G] [topological_space G] [has_continuous_sub G] (h : is_closed {x : G | 0 ≤ x}) :
is_closed {p : G × G | p.fst ≤ p.snd}
source
@[protected, instance]
def normed_lattice_add_comm_group.order_closed_topology {E : Type u_1} [normed_lattice_add_comm_group E] :
order_closed_topology E