Extended norm

ATTENTION. This file is deprecated. Mathlib now has classes ENormed(Add)(Comm)Monoid for (additive) (commutative) monoids with an ENorm: this is very similar to this definition, but much more general. Should the need arise, an enormed version of a normed space can be added later: this will be different from this file.

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

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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 }

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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, deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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, deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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, deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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

@[simp, deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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, deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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)

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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_ge := ⋯, 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 := ⊤ }

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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, deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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)

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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, deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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 := ⋯ }

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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 ⋯

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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 := ⋯ }

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]

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 := ⋯ }