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 𝕜] [AddCommGroup V] [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) ≤ ↑‖c‖₊ * ↑self x

theorem ENorm.eq_zero' {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [Module 𝕜 V] (self : ENorm 𝕜 V) (c : 𝕜) (x : V) : ↑self (c • x) ≤ ↑‖c‖₊ * ↑self x

instance ENorm.instCoeFunForallENNReal {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [Module 𝕜 V] : Function.Injective ENorm.toFun

theorem ENorm.ext {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [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} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENorm 𝕜 V) : ↑e 0 = 0

@[simp]

theorem ENorm.eq_zero_iff {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENorm 𝕜 V) (x : V) : ↑e (-x) = ↑e x

theorem ENorm.map_sub_rev {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [Module 𝕜 V] : PartialOrder (ENorm 𝕜 V)

Equations

• ENorm.partialOrder = PartialOrder.mk ⋯

noncomputable instance ENorm.instTop {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [Module 𝕜 V] : Inhabited (ENorm 𝕜 V)

Equations

• ENorm.instInhabited = { default := ⊤ }

theorem ENorm.top_map {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] {x : V} (hx : x ≠ 0) : ↑⊤ x = ⊤

noncomputable instance ENorm.instOrderTop {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] : OrderTop (ENorm 𝕜 V)

Equations

• ENorm.instOrderTop = OrderTop.mk ⋯

noncomputable instance ENorm.instSemilatticeSup {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENorm 𝕜 V) : EMetricSpace V

Structure of an EMetricSpace defined by an extended norm.

Equations

• e.emetricSpace = EMetricSpace.mk ⋯

def ENorm.finiteSubspace {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [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' := ⋯ }

instance ENorm.metricSpace {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [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 = EMetricSpace.toMetricSpace ⋯

theorem ENorm.finite_dist_eq {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [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 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENorm 𝕜 V) : NormedAddCommGroup ↥e.finiteSubspace

Normed group instance on e.finiteSubspace.

Equations

• e.normedAddCommGroup = let __src := e.metricSpace; NormedAddCommGroup.mk ⋯

theorem ENorm.finite_norm_eq {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENorm 𝕜 V) (x : ↥e.finiteSubspace) : ‖x‖ = (↑e ↑x).toReal

instance ENorm.normedSpace {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENorm 𝕜 V) : NormedSpace 𝕜 ↥e.finiteSubspace

Normed space instance on e.finiteSubspace.

Equations

• e.normedSpace = NormedSpace.mk ⋯