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
emetric_spacestructure onVcorresponding toe : enorm š V;- the subspace of vectors with finite norm, called
e.finite_subspace; - a
normed_spacestructure 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]
[vector_space š V] :
Type u_2
- to_fun : V ā ennreal
- eq_zero' : ā (x : V), c.to_fun x = 0 ā x = 0
- map_add_le' : ā (x y : V), c.to_fun (x + y) ā¤ c.to_fun x + c.to_fun y
- map_smul_le' : ā (c_1 : š) (x : V), c.to_fun (c_1 ā¢ x) ā¤ ā(nnnorm c_1) * c.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.
@[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
- enorm.has_coe_to_fun = {F := Ī» (x : enorm š V), V ā ennreal, coe := enorm.to_fun _inst_3}
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ā¦ :
@[ext]
theorem
enorm.ext
{š : Type u_1}
{V : Type u_2}
[normed_field š]
[add_comm_group V]
[vector_space š V]
{eā eā : enorm š V} :
theorem
enorm.ext_iff
{š : Type u_1}
{V : Type u_2}
[normed_field š]
[add_comm_group V]
[vector_space š V]
{eā eā : enorm š V} :
@[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) :
@[simp]
theorem
enorm.map_zero
{š : Type u_1}
{V : Type u_2}
[normed_field š]
[add_comm_group V]
[vector_space š V]
(e : enorm š V) :
@[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} :
@[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) :
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) :
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) :
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) :
@[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)
@[instance]
def
enorm.has_top
{š : Type u_1}
{V : Type u_2}
[normed_field š]
[add_comm_group V]
[vector_space š 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' := _}}
@[instance]
def
enorm.inhabited
{š : Type u_1}
{V : Type u_2}
[normed_field š]
[add_comm_group V]
[vector_space š V] :
Equations
- enorm.inhabited = {default := ā¤}
theorem
enorm.top_map
{š : Type u_1}
{V : Type u_2}
[normed_field š]
[add_comm_group V]
[vector_space š V]
{x : V} :
@[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
- enorm.semilattice_sup_top = {top := ā¤, 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_top := _, sup := Ī» (eā eā : enorm š V), {to_fun := Ī» (x : V), max (āeā x) (āeā x), eq_zero' := _, map_add_le' := _, map_smul_le' := _}, le_sup_left := _, le_sup_right := _, sup_le := _}
@[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) :
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) :
def
enorm.emetric_space
{š : Type u_1}
{V : Type u_2}
[normed_field š]
[add_comm_group V]
[vector_space š V] :
enorm š V ā emetric_space V
Structure of an emetric_space defined by an extended norm.
Equations
- e.emetric_space = {to_has_edist := {edist := Ī» (x y : V), āe (x - y)}, edist_self := _, eq_of_edist_eq_zero := _, edist_comm := _, edist_triangle := _, to_uniform_space := uniform_space_of_edist (Ī» (x y : V), āe (x - y)) _ _ _, uniformity_edist := _}
def
enorm.finite_subspace
{š : Type u_1}
{V : Type u_2}
[normed_field š]
[add_comm_group V]
[vector_space š V] :
The subspace of vectors with finite enorm.
@[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 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
- e.metric_space = let _inst : emetric_space V := e.emetric_space in emetric_space.to_metric_space_of_dist (Ī» (x y : ā„(e.finite_subspace)), (has_edist.edist x y).to_real) _ _
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)) :
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)) :
@[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 instance on e.finite_subspace.
Equations
- e.normed_group = {to_has_norm := {norm := Ī» (x : ā„(e.finite_subspace)), (āe āx).to_real}, to_add_comm_group := submodule.add_comm_group e.finite_subspace, to_metric_space := e.metric_space, dist_eq := _}
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)) :
@[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
- e.normed_space = {to_semimodule := submodule.semimodule e.finite_subspace, norm_smul_le := _}