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

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

@[instance]
def enorm.has_coe_to_fun {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :
has_coe_to_fun (enorm 𝕜 V)
Equations
theorem enorm.coe_fn_injective {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :
function.injective (λ (e : enorm 𝕜 V) (x : V), ⇑e x)
@[ext]
theorem enorm.ext {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] {e₁ e₂ : enorm 𝕜 V} (h : ∀ (x : V), ⇑e₁ x = ⇑e₂ x) :
e₁ = e₂
theorem enorm.ext_iff {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] {e₁ e₂ : enorm 𝕜 V} :
e₁ = e₂ ↔ ∀ (x : V), ⇑e₁ x = ⇑e₂ x
@[simp]
theorem enorm.coe_inj {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] {e₁ e₂ : enorm 𝕜 V} :
⇑e₁ = ⇑e₂ ↔ e₁ = e₂
@[simp]
theorem enorm.map_smul {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) (c : 𝕜) (x : V) :
@[simp]
theorem enorm.map_zero {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) :
⇑e 0 = 0
@[simp]
theorem enorm.eq_zero_iff {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group 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} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) (x : V) :
⇑e (-x) = ⇑e x
theorem enorm.map_sub_rev {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) (x y : V) :
⇑e (x - y) = ⇑e (y - x)
theorem enorm.map_add_le {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) (x y : V) :
⇑e (x + y) ≤ ⇑e x + ⇑e y
theorem enorm.map_sub_le {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) (x y : V) :
⇑e (x - y) ≤ ⇑e x + ⇑e y
@[instance]
def enorm.partial_order {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :
partial_order (enorm 𝕜 V)
Equations
@[instance]
def enorm.has_top {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :
has_top (enorm 𝕜 V)

The enorm sending each non-zero vector to infinity.

Equations
@[instance]
def enorm.inhabited {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :
inhabited (enorm 𝕜 V)
Equations
theorem enorm.top_map {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] {x : V} (hx : x ≠ 0) :
@[instance]
def enorm.semilattice_sup_top {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :
Equations
@[simp]
theorem enorm.coe_max {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e₁ e₂ : enorm 𝕜 V) :
⇑(e₁ ⊔ e₂) = λ (x : V), max (⇑e₁ x) (⇑e₂ x)
theorem enorm.max_map {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e₁ e₂ : enorm 𝕜 V) (x : V) :
⇑(e₁ ⊔ e₂) x = max (⇑e₁ x) (⇑e₂ x)
def enorm.emetric_space {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) :

Structure of an emetric_space defined by an extended norm.

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

The subspace of vectors with finite enorm.

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

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
theorem enorm.finite_dist_eq {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) (x y : ↥(e.finite_subspace)) :
theorem enorm.finite_edist_eq {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) (x y : ↥(e.finite_subspace)) :
@[instance]
def enorm.finite_subspace.normed_group {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) :

Normed group instance on e.finite_subspace.

Equations
theorem enorm.finite_norm_eq {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) (x : ↥(e.finite_subspace)) :
@[instance]
def enorm.finite_subspace.normed_space {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] (e : enorm 𝕜 V) :

Normed space instance on e.finite_subspace.

Equations