mathlib3 documentation

analysis.normed_space.enorm

Extended norm #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

emetric_space structure on V corresponding to e : enorm 𝕜 V;
the subspace of vectors with finite norm, called e.finite_subspace;
a normed_space 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) [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :

Type u_2

to_fun : V → ennreal
eq_zero' : ∀ (x : V), self.to_fun x = 0 → x = 0
map_add_le' : ∀ (x y : V), self.to_fun (x + y) ≤ self.to_fun x + self.to_fun y
map_smul_le' : ∀ (c : 𝕜) (x : V), self.to_fun (c • x) ≤ ↑‖c‖₊ * self.to_fun x

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.

Instances for enorm

@[protected, 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) (λ (_x : enorm 𝕜 V), V → ennreal)

Equations

enorm.has_coe_to_fun = {coe := enorm.to_fun _inst_3}

theorem enorm.coe_fn_injective {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :

function.injective coe_fn

@[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, norm_cast]

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) :

⇑e (c • x) = ↑‖c‖₊ * ⇑e x

@[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

@[protected, 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

enorm.partial_order = {le := λ (e₁ e₂ : enorm 𝕜 V), ∀ (x : V), ⇑e₁ x ≤ ⇑e₂ x, lt := preorder.lt._default (λ (e₁ e₂ : enorm 𝕜 V), ∀ (x : V), ⇑e₁ x ≤ ⇑e₂ x), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[protected, instance]

noncomputable 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

enorm.has_top = {top := {to_fun := λ (x : V), ite (x = 0) 0 ⊤, eq_zero' := _, map_add_le' := _, map_smul_le' := _}}

@[protected, instance]

noncomputable def enorm.inhabited {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :

inhabited (enorm 𝕜 V)

Equations

enorm.inhabited = {default := ⊤}

theorem enorm.top_map {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] {x : V} (hx : x ≠ 0) :

@[protected, instance]

noncomputable def enorm.order_top {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :

order_top (enorm 𝕜 V)

Equations

enorm.order_top = {top := ⊤, le_top := _}

@[protected, instance]

noncomputable def enorm.semilattice_sup {𝕜 : Type u_1} {V : Type u_2} [normed_field 𝕜] [add_comm_group V] [module 𝕜 V] :

semilattice_sup (enorm 𝕜 V)

Equations

enorm.semilattice_sup = {sup := λ (e₁ e₂ : enorm 𝕜 V), {to_fun := λ (x : V), linear_order.max (⇑e₁ x) (⇑e₂ x), eq_zero' := _, map_add_le' := _, map_smul_le' := _}, le := has_le.le (preorder.to_has_le (enorm 𝕜 V)), lt := has_lt.lt (preorder.to_has_lt (enorm 𝕜 V)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

@[simp, norm_cast]

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), linear_order.max (⇑e₁ x) (⇑e₂ x)

@[norm_cast]

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 = linear_order.max (⇑e₁ x) (⇑e₂ x)

@[reducible]

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

emetric_space V

Structure of an emetric_space defined by an extended norm.

Equations

e.emetric_space = {to_pseudo_emetric_space := {to_has_edist := {edist := λ (x y : V), ⇑e (x - y)}, edist_self := _, edist_comm := _, edist_triangle := _, to_uniform_space := uniform_space_of_edist (λ (x y : V), ⇑e (x - y)) _ _ _, uniformity_edist := _}, eq_of_edist_eq_zero := _}

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

e.finite_subspace = {carrier := {x : V | ⇑e x < ⊤}, add_mem' := _, zero_mem' := _, smul_mem' := _}

Instances for ↥enorm.finite_subspace

@[protected, instance]

noncomputable 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 ↥(e.finite_subspace)

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

Equations

enorm.finite_subspace.metric_space e = let _inst : emetric_space V := e.emetric_space in emetric_space.to_metric_space _

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)) :

has_dist.dist x y = (⇑e (↑x - ↑y)).to_real

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)) :

has_edist.edist x y = ⇑e (↑x - ↑y)

@[protected, instance]

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

normed_add_comm_group ↥(e.finite_subspace)

Normed group instance on e.finite_subspace.

Equations

enorm.finite_subspace.normed_add_comm_group e = {to_has_norm := {norm := λ (x : ↥(e.finite_subspace)), (⇑e ↑x).to_real}, to_add_comm_group := {add := add_comm_group.add (submodule.add_comm_group e.finite_subspace), add_assoc := _, zero := add_comm_group.zero (submodule.add_comm_group e.finite_subspace), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (submodule.add_comm_group e.finite_subspace), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (submodule.add_comm_group e.finite_subspace), sub := add_comm_group.sub (submodule.add_comm_group e.finite_subspace), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (submodule.add_comm_group e.finite_subspace), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}, to_metric_space := {to_pseudo_metric_space := metric_space.to_pseudo_metric_space (enorm.finite_subspace.metric_space e), eq_of_dist_eq_zero := _}, dist_eq := _}

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)) :

‖x‖ = (⇑e ↑x).to_real

@[protected, 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 𝕜 ↥(e.finite_subspace)

Normed space instance on e.finite_subspace.

Equations

enorm.finite_subspace.normed_space e = {to_module := submodule.module e.finite_subspace, norm_smul_le := _}