# Extended norm #

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

• EMetricSpace structure on V corresponding to e : ENorm š V;
• the subspace of vectors with finite norm, called e.finiteSubspace;
• a NormedSpace 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) [NormedField š] [] [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.

• toFun : V ā ENNReal
• eq_zero' : ā (x : V), āself x = 0 ā x = 0
• map_add_le' : ā (x y : V), āself (x + y) ā¤ āself x + āself y
• map_smul_le' : ā (c : š) (x : V), āself (c ā¢ x) ā¤ ā * āself x
Instances For
theorem ENorm.eq_zero' {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (self : ENorm š V) (x : V) :
āself x = 0 ā x = 0
theorem ENorm.map_add_le' {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (self : ENorm š V) (x : V) (y : V) :
āself (x + y) ā¤ āself x + āself y
theorem ENorm.map_smul_le' {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (self : ENorm š V) (c : š) (x : V) :
āself (c ā¢ x) ā¤ ā * āself x
instance ENorm.instCoeFunForallENNReal {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] :
CoeFun (ENorm š V) fun (x : ENorm š V) => V ā ENNReal
Equations
• ENorm.instCoeFunForallENNReal = { coe := ENorm.toFun }
theorem ENorm.coeFn_injective {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] :
Function.Injective ENorm.toFun
theorem ENorm.ext {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] {eā : ENorm š V} {eā : ENorm š V} (h : ā (x : V), āeā x = āeā x) :
eā = eā
theorem ENorm.ext_iff {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] {eā : ENorm š V} {eā : ENorm š V} :
eā = eā ā ā (x : V), āeā x = āeā x
@[simp]
theorem ENorm.coe_inj {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] {eā : ENorm š V} {eā : ENorm š V} :
āeā = āeā ā eā = eā
@[simp]
theorem ENorm.map_smul {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) (c : š) (x : V) :
āe (c ā¢ x) = ā * āe x
@[simp]
theorem ENorm.map_zero {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) :
āe 0 = 0
@[simp]
theorem ENorm.eq_zero_iff {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) {x : V} :
āe x = 0 ā x = 0
@[simp]
theorem ENorm.map_neg {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) (x : V) :
āe (-x) = āe x
theorem ENorm.map_sub_rev {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) (x : V) (y : V) :
āe (x - y) = āe (y - x)
theorem ENorm.map_add_le {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) (x : V) (y : V) :
āe (x + y) ā¤ āe x + āe y
theorem ENorm.map_sub_le {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) (x : V) (y : V) :
āe (x - y) ā¤ āe x + āe y
instance ENorm.partialOrder {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] :
PartialOrder (ENorm š V)
Equations
• ENorm.partialOrder =
noncomputable instance ENorm.instTop {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] :
Top (ENorm š V)

The ENorm sending each non-zero vector to infinity.

Equations
• ENorm.instTop = { top := { toFun := fun (x : V) => if x = 0 then 0 else ā¤, eq_zero' := āÆ, map_add_le' := āÆ, map_smul_le' := āÆ } }
noncomputable instance ENorm.instInhabited {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] :
Inhabited (ENorm š V)
Equations
• ENorm.instInhabited = { default := ā¤ }
theorem ENorm.top_map {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] {x : V} (hx : x ā  0) :
āā¤ x = ā¤
noncomputable instance ENorm.instOrderTop {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] :
OrderTop (ENorm š V)
Equations
noncomputable instance ENorm.instSemilatticeSup {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] :
SemilatticeSup (ENorm š V)
Equations
• ENorm.instSemilatticeSup = let __src := ENorm.partialOrder; SemilatticeSup.mk āÆ āÆ āÆ
@[simp]
theorem ENorm.coe_max {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (eā : ENorm š V) (eā : ENorm š V) :
ā(eā ā eā) = fun (x : V) => max (āeā x) (āeā x)
theorem ENorm.max_map {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (eā : ENorm š V) (eā : ENorm š V) (x : V) :
ā(eā ā eā) x = max (āeā x) (āeā x)
@[reducible, inline]
abbrev ENorm.emetricSpace {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) :

Structure of an EMetricSpace defined by an extended norm.

Equations
• e.emetricSpace =
Instances For
def ENorm.finiteSubspace {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) :
Subspace š V

The subspace of vectors with finite enorm.

Equations
• e.finiteSubspace = { carrier := {x : V | āe x < ā¤}, add_mem' := āÆ, zero_mem' := āÆ, smul_mem' := āÆ }
Instances For
instance ENorm.metricSpace {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) :
MetricSpace ā„e.finiteSubspace

Metric space structure on e.finiteSubspace. We use EMetricSpace.toMetricSpace to ensure that this definition agrees with e.emetricSpace.

Equations
• e.metricSpace =
theorem ENorm.finite_dist_eq {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) (x : ā„e.finiteSubspace) (y : ā„e.finiteSubspace) :
dist x y = (āe (āx - āy)).toReal
theorem ENorm.finite_edist_eq {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) (x : ā„e.finiteSubspace) (y : ā„e.finiteSubspace) :
edist x y = āe (āx - āy)
instance ENorm.normedAddCommGroup {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) :

Normed group instance on e.finiteSubspace.

Equations
• e.normedAddCommGroup = let __src := e.metricSpace;
theorem ENorm.finite_norm_eq {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) (x : ā„e.finiteSubspace) :
= (āe āx).toReal
instance ENorm.normedSpace {š : Type u_1} {V : Type u_2} [NormedField š] [] [Module š V] (e : ENorm š V) :
NormedSpace š ā„e.finiteSubspace

Normed space instance on e.finiteSubspace.

Equations
• e.normedSpace =