mathlib documentation

analysis.normed_space.dual

The topological dual of a normed space

In this file we define the topological dual of a normed space, and the bounded linear map from a normed space into its double dual.

We also prove that, for base field such as the real or the complex numbers, this map is an isometry. More generically, this is proved for any field in the class has_exists_extension_norm_eq, i.e., satisfying the Hahn-Banach theorem.

@[instance]
def normed_space.dual.normed_group (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] :

def normed_space.dual (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] :
Type (max u_2 u_1)

The topological dual of a normed space E.

Equations
@[instance]
def normed_space.dual.has_coe_to_fun (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] :

@[instance]
def normed_space.dual.inst (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] :
normed_space π•œ (normed_space.dual π•œ E)

@[instance]
def normed_space.inhabited (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] :

Equations
def normed_space.inclusion_in_double_dual' (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] :
E β†’ normed_space.dual π•œ (normed_space.dual π•œ E)

The inclusion of a normed space in its double (topological) dual.

Equations
@[simp]
theorem normed_space.dual_def (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] (x : E) (f : normed_space.dual π•œ E) :

theorem normed_space.double_dual_bound (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] (x : E) :

def normed_space.inclusion_in_double_dual (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] :
E β†’L[π•œ] normed_space.dual π•œ (normed_space.dual π•œ E)

The inclusion of a normed space in its double (topological) dual, considered as a bounded linear map.

Equations
theorem normed_space.norm_le_dual_bound {π•œ : Type v} [nondiscrete_normed_field π•œ] [normed_algebra ℝ π•œ] [has_exists_extension_norm_eq π•œ] {E : Type u} [normed_group E] [normed_space π•œ E] (x : E) {M : ℝ} :
0 ≀ M β†’ (βˆ€ (f : normed_space.dual π•œ E), βˆ₯⇑f xβˆ₯ ≀ M * βˆ₯fβˆ₯) β†’ βˆ₯xβˆ₯ ≀ M

If one controls the norm of every f x, then one controls the norm of x. Compare continuous_linear_map.op_norm_le_bound.

The inclusion of a real normed space in its double dual is an isometry onto its image.