mathlib documentation

analysis.normed_space.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

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

source
structure enorm (𝕜 : Type u_1) (V : Type u_2) [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 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.

source
@[instance]
def enorm.has_coe_to_fun {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] :
has_coe_to_fun (enorm 𝕜 V)

Equations
source
theorem enorm.coe_fn_injective {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] ⦃e₁ e₂ : enorm 𝕜 V⦄ (h : ⇑e₁ = ⇑e₂) :
e₁ = e₂

source
@[ext]
theorem enorm.ext {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] {e₁ e₂ : enorm 𝕜 V} (h : ∀ (x : V), ⇑e₁ x = ⇑e₂ x) :
e₁ = e₂

source
theorem enorm.ext_iff {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] {e₁ e₂ : enorm 𝕜 V} :
e₁ = e₂ ↔ ∀ (x : V), ⇑e₁ x = ⇑e₂ x

source
@[simp]
theorem enorm.map_smul {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) (c : 𝕜) (x : V) :
⇑e (c • x) = (↑(nnnorm c)) * ⇑e x

source
@[simp]
theorem enorm.map_zero {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) :
⇑e 0 = 0

source
@[simp]
theorem enorm.eq_zero_iff {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) {x : V} :
⇑e x = 0 ↔ x = 0

source
@[simp]
theorem enorm.map_neg {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) (x : V) :
⇑e (-x) = ⇑e x

source
theorem enorm.map_sub_rev {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) (x y : V) :
⇑e (x - y) = ⇑e (y - x)

source
theorem enorm.map_add_le {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) (x y : V) :
⇑e (x + y) ≤ ⇑e x + ⇑e y

source
theorem enorm.map_sub_le {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) (x y : V) :
⇑e (x - y) ≤ ⇑e x + ⇑e y

source
@[instance]
def enorm.partial_order {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] :
partial_order (enorm 𝕜 V)

Equations
source
@[instance]
def enorm.has_top {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] :
has_top (enorm 𝕜 V)

The enorm sending each non-zero vector to infinity.

Equations
source
@[instance]
def enorm.inhabited {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] :
inhabited (enorm 𝕜 V)

Equations
source
theorem enorm.top_map {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] {x : V} (hx : x ≠ 0) :
⇑⊤ x = ⊤

source
@[instance]
def enorm.semilattice_sup_top {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] :
semilattice_sup_top (enorm 𝕜 V)

Equations
source
@[simp]
theorem enorm.coe_max {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e₁ e₂ : enorm 𝕜 V) :
⇑(e₁ ⊔ e₂) = λ (x : V), max (⇑e₁ x) (⇑e₂ x)

source
theorem enorm.max_map {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e₁ e₂ : enorm 𝕜 V) (x : V) :
⇑(e₁ ⊔ e₂) x = max (⇑e₁ x) (⇑e₂ x)

source
def enorm.emetric_space {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) :
emetric_space V

Structure of an emetric_space defined by an extended norm.

Equations
source
def enorm.finite_subspace {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) :
subspace 𝕜 V

The subspace of vectors with finite enorm.

Equations
source
@[instance]
def enorm.metric_space {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) :
metric_space ↥(e.finite_subspace)

Metric space structure on e.finite_subspace. We use emetric_space.to_metric_space_of_dist to ensure that this definition agrees with e.emetric_space.

Equations
source
theorem enorm.finite_dist_eq {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) (x y : ↥(e.finite_subspace)) :
dist x y = (⇑e (↑x - ↑y)).to_real

source
theorem enorm.finite_edist_eq {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) (x y : ↥(e.finite_subspace)) :
edist x y = ⇑e (↑x - ↑y)

source
@[instance]
def enorm.normed_group {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) :
normed_group ↥(e.finite_subspace)

Normed group instance on e.finite_subspace.

Equations
source
theorem enorm.finite_norm_eq {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) (x : ↥(e.finite_subspace)) :
∥x∥ = (⇑e ↑x).to_real

source
@[instance]
def enorm.normed_space {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [vector_space 𝕜 V] (e : enorm 𝕜 V) :
normed_space 𝕜 ↥(e.finite_subspace)

Normed space instance on e.finite_subspace.

Equations