Extended norm

In this file we define a structure ENormedSpace 𝕜 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 ENormedSpace 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 : ENormedSpace 𝕜 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 ENormedSpace (𝕜 : 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

  the norm of an ENormedSpace, taking values into ℝ≥0∞

• 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

instance ENormedSpace.instCoeFunForallENNReal {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] : CoeFun (ENormedSpace 𝕜 V) fun (x : ENormedSpace 𝕜 V) => V → ENNReal

Equations

• ENormedSpace.instCoeFunForallENNReal = { coe := ENormedSpace.toFun }

theorem ENormedSpace.coeFn_injective {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] : Function.Injective toFun

theorem ENormedSpace.ext {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] {e₁ e₂ : ENormedSpace 𝕜 V} (h : ∀ (x : V), ↑e₁ x = ↑e₂ x) : e₁ = e₂

theorem ENormedSpace.ext_iff {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] {e₁ e₂ : ENormedSpace 𝕜 V} : e₁ = e₂ ↔ ∀ (x : V), ↑e₁ x = ↑e₂ x

@[simp]

theorem ENormedSpace.coe_inj {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] {e₁ e₂ : ENormedSpace 𝕜 V} : ↑e₁ = ↑e₂ ↔ e₁ = e₂

@[simp]

theorem ENormedSpace.map_smul {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) (c : 𝕜) (x : V) : ↑e (c • x) = ↑‖c‖₊ * ↑e x

@[simp]

theorem ENormedSpace.map_zero {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) : ↑e 0 = 0

@[simp]

theorem ENormedSpace.eq_zero_iff {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) {x : V} : ↑e x = 0 ↔ x = 0

@[simp]

theorem ENormedSpace.map_neg {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) (x : V) : ↑e (-x) = ↑e x

theorem ENormedSpace.map_sub_rev {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) (x y : V) : ↑e (x - y) = ↑e (y - x)

theorem ENormedSpace.map_add_le {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) (x y : V) : ↑e (x + y) ≤ ↑e x + ↑e y

theorem ENormedSpace.map_sub_le {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) (x y : V) : ↑e (x - y) ≤ ↑e x + ↑e y

instance ENormedSpace.partialOrder {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] : PartialOrder (ENormedSpace 𝕜 V)

Equations

• ENormedSpace.partialOrder = { le := fun (e₁ e₂ : ENormedSpace 𝕜 V) => ∀ (x : V), ↑e₁ x ≤ ↑e₂ x, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯, le_antisymm := ⋯ }

noncomputable instance ENormedSpace.instTop {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] : Top (ENormedSpace 𝕜 V)

The ENormedSpace sending each non-zero vector to infinity.

Equations

• ENormedSpace.instTop = { top := { toFun := fun (x : V) => if x = 0 then 0 else ⊤, eq_zero' := ⋯, map_add_le' := ⋯, map_smul_le' := ⋯ } }

noncomputable instance ENormedSpace.instInhabited {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] : Inhabited (ENormedSpace 𝕜 V)

Equations

• ENormedSpace.instInhabited = { default := ⊤ }

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

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

Equations

• ENormedSpace.instOrderTop = { toTop := ENormedSpace.instTop, le_top := ⋯ }

noncomputable instance ENormedSpace.instSemilatticeSup {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] : SemilatticeSup (ENormedSpace 𝕜 V)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ENormedSpace.coe_max {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e₁ e₂ : ENormedSpace 𝕜 V) : ↑(e₁ ⊔ e₂) = fun (x : V) => max (↑e₁ x) (↑e₂ x)

theorem ENormedSpace.max_map {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e₁ e₂ : ENormedSpace 𝕜 V) (x : V) : ↑(e₁ ⊔ e₂) x = max (↑e₁ x) (↑e₂ x)

@[reducible, inline]

abbrev ENormedSpace.emetricSpace {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) : EMetricSpace V

Structure of an EMetricSpace defined by an extended norm.

Equations

• e.emetricSpace = { edist := fun (x y : V) => ↑e (x - y), edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, uniformity_edist := ⋯, eq_of_edist_eq_zero := ⋯ }

def ENormedSpace.finiteSubspace {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) : Subspace 𝕜 V

The subspace of vectors with finite ENormedSpace.

Equations

• e.finiteSubspace = { carrier := {x : V | ↑e x < ⊤}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

instance ENormedSpace.metricSpace {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 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 ENormedSpace.finite_dist_eq {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) (x y : ↥e.finiteSubspace) : dist x y = (↑e (↑x - ↑y)).toReal

theorem ENormedSpace.finite_edist_eq {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) (x y : ↥e.finiteSubspace) : edist x y = ↑e (↑x - ↑y)

instance ENormedSpace.normedAddCommGroup {𝕜 : Type u_1} {V : Type u_2} [NormedField 𝕜] [AddCommGroup V] [Module 𝕜 V] (e : ENormedSpace 𝕜 V) : NormedAddCommGroup ↥e.finiteSubspace

Normed group instance on e.finiteSubspace.

Equations

• e.normedAddCommGroup = { norm := fun (x : ↥e.finiteSubspace) => (↑e ↑x).toReal, toAddCommGroup := Submodule.addCommGroup e.finiteSubspace, toMetricSpace := e.metricSpace, dist_eq := ⋯ }

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

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

Normed space instance on e.finiteSubspace.

Equations

• e.normedSpace = { toModule := Submodule.module e.finiteSubspace, norm_smul_le := ⋯ }