# mathlib3documentation

analysis.normed_space.enorm

# Extended norm #

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

In this file we define a structure enorm π V representing an extended norm (i.e., a norm that can take the value β) on a vector space V over a normed field π. We do not use class for an enorm because the same space can have more than one extended norm. For example, the space of measurable functions f : Ξ± β β has a family of L_p extended norms.

We prove some basic inequalities, then define

• emetric_space structure on V corresponding to e : enorm π V;
• the subspace of vectors with finite norm, called e.finite_subspace;
• a normed_space structure on this space.

The last definition is an instance because the type involves e.

## Implementation notes #

We do not define extended normed groups. They can be added to the chain once someone will need them.

## Tags #

normed space, extended norm

structure enorm (π : Type u_1) (V : Type u_2) [normed_field π] [module π V] :
Type u_2

Extended norm on a vector space. As in the case of normed spaces, we require only βc β’ xβ β€ βcβ * βxβ in the definition, then prove an equality in map_smul.

Instances for enorm
@[protected, instance]
def enorm.has_coe_to_fun {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] :
has_coe_to_fun (enorm π V) (Ξ» (_x : enorm π V),
Equations
theorem enorm.coe_fn_injective {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] :
@[ext]
theorem enorm.ext {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] {eβ eβ : enorm π V} (h : β (x : V), βeβ x = βeβ x) :
eβ = eβ
theorem enorm.ext_iff {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] {eβ eβ : enorm π V} :
eβ = eβ β β (x : V), βeβ x = βeβ x
@[simp, norm_cast]
theorem enorm.coe_inj {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] {eβ eβ : enorm π V} :
βeβ = βeβ β eβ = eβ
@[simp]
theorem enorm.map_smul {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) (c : π) (x : V) :
@[simp]
theorem enorm.map_zero {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) :
βe 0 = 0
@[simp]
theorem enorm.eq_zero_iff {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) {x : V} :
βe x = 0 β x = 0
@[simp]
theorem enorm.map_neg {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) (x : V) :
βe (-x) = βe x
theorem enorm.map_sub_rev {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) (x y : V) :
βe (x - y) = βe (y - x)
theorem enorm.map_add_le {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) (x y : V) :
βe (x + y) β€ βe x + βe y
theorem enorm.map_sub_le {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) (x y : V) :
βe (x - y) β€ βe x + βe y
@[protected, instance]
def enorm.partial_order {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] :
partial_order (enorm π V)
Equations
@[protected, instance]
noncomputable def enorm.has_top {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] :
has_top (enorm π V)

The enorm sending each non-zero vector to infinity.

Equations
@[protected, instance]
noncomputable def enorm.inhabited {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] :
inhabited (enorm π V)
Equations
theorem enorm.top_map {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] {x : V} (hx : x β  0) :
@[protected, instance]
noncomputable def enorm.order_top {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] :
order_top (enorm π V)
Equations
@[protected, instance]
noncomputable def enorm.semilattice_sup {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] :
semilattice_sup (enorm π V)
Equations
@[simp, norm_cast]
theorem enorm.coe_max {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (eβ eβ : enorm π V) :
β(eβ β eβ) = Ξ» (x : V), linear_order.max (βeβ x) (βeβ x)
@[norm_cast]
theorem enorm.max_map {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (eβ eβ : enorm π V) (x : V) :
β(eβ β eβ) x = linear_order.max (βeβ x) (βeβ x)
@[reducible]
noncomputable def enorm.emetric_space {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) :

Structure of an emetric_space defined by an extended norm.

Equations
def enorm.finite_subspace {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) :
subspace π V

The subspace of vectors with finite enorm.

Equations
Instances for β₯enorm.finite_subspace
@[protected, instance]
noncomputable def enorm.finite_subspace.metric_space {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) :

Metric space structure on e.finite_subspace. We use emetric_space.to_metric_space to ensure that this definition agrees with e.emetric_space.

Equations
theorem enorm.finite_dist_eq {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) (x y : β₯(e.finite_subspace)) :
theorem enorm.finite_edist_eq {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) (x y : β₯(e.finite_subspace)) :
@[protected, instance]
noncomputable def enorm.finite_subspace.normed_add_comm_group {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) :

Normed group instance on e.finite_subspace.

Equations
theorem enorm.finite_norm_eq {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) (x : β₯(e.finite_subspace)) :
@[protected, instance]
def enorm.finite_subspace.normed_space {π : Type u_1} {V : Type u_2} [normed_field π] [module π V] (e : enorm π V) :

Normed space instance on e.finite_subspace.

Equations