# Documentation

Mathlib.Analysis.NormedSpace.ENorm

# 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) [] [] [Module 𝕜 V] :
Type u_2
• toFun : VENNReal
• eq_zero' : ∀ (x : V), s x = 0x = 0
• map_add_le' : ∀ (x y : V), s (x + y) s x + s y
• map_smul_le' : ∀ (c : 𝕜) (x : V), s (c x) c‖₊ * s x

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
instance ENorm.instCoeFunENormForAllENNReal {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] :
CoeFun (ENorm 𝕜 V) fun x => VENNReal
theorem ENorm.coeFn_injective {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] :
Function.Injective ENorm.toFun
theorem ENorm.ext {𝕜 : Type u_1} {V : Type u_2} [] [] [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} [] [] [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} [] [] [Module 𝕜 V] {e₁ : ENorm 𝕜 V} {e₂ : ENorm 𝕜 V} :
e₁ = e₂ e₁ = e₂
@[simp]
theorem ENorm.map_smul {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) (c : 𝕜) (x : V) :
e (c x) = c‖₊ * e x
@[simp]
theorem ENorm.map_zero {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) :
e 0 = 0
@[simp]
theorem ENorm.eq_zero_iff {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) {x : V} :
e x = 0 x = 0
@[simp]
theorem ENorm.map_neg {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) (x : V) :
e (-x) = e x
theorem ENorm.map_sub_rev {𝕜 : Type u_1} {V : Type u_2} [] [] [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} [] [] [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} [] [] [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} [] [] [Module 𝕜 V] :
noncomputable instance ENorm.instTopENorm {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] :
Top (ENorm 𝕜 V)

The ENorm sending each non-zero vector to infinity.

noncomputable instance ENorm.instInhabitedENorm {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] :
Inhabited (ENorm 𝕜 V)
theorem ENorm.top_map {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] {x : V} (hx : x 0) :
x =
noncomputable instance ENorm.instOrderTopENormToLEToPreorderPartialOrder {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] :
OrderTop (ENorm 𝕜 V)
noncomputable instance ENorm.instSemilatticeSupENorm {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] :
@[simp]
theorem ENorm.coe_max {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e₁ : ENorm 𝕜 V) (e₂ : ENorm 𝕜 V) :
↑(e₁ e₂) = fun x => max (e₁ x) (e₂ x)
theorem ENorm.max_map {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e₁ : ENorm 𝕜 V) (e₂ : ENorm 𝕜 V) (x : V) :
↑(e₁ e₂) x = max (e₁ x) (e₂ x)
@[reducible]
def ENorm.emetricSpace {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) :

Structure of an EMetricSpace defined by an extended norm.

Instances For
def ENorm.finiteSubspace {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) :
Subspace 𝕜 V

The subspace of vectors with finite enorm.

Instances For
instance ENorm.metricSpace {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) :
MetricSpace { x // }

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

theorem ENorm.finite_dist_eq {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) (x : { x // }) (y : { x // }) :
dist x y = ENNReal.toReal (e (x - y))
theorem ENorm.finite_edist_eq {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) (x : { x // }) (y : { x // }) :
edist x y = e (x - y)
instance ENorm.normedAddCommGroup {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) :

Normed group instance on e.finiteSubspace.

theorem ENorm.finite_norm_eq {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) (x : { x // }) :
x = ENNReal.toReal (e x)
instance ENorm.normedSpace {𝕜 : Type u_1} {V : Type u_2} [] [] [Module 𝕜 V] (e : ENorm 𝕜 V) :
NormedSpace 𝕜 { x // }

Normed space instance on e.finiteSubspace.