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.

source

@[instance]

def normed_space.dual.normed_group (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (E : Type u_2) [normed_group E] [normed_space 𝕜 E] :

normed_group (normed_space.dual 𝕜 E)

source

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

normed_space.dual 𝕜 E = (E →L[𝕜] 𝕜)

source

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

has_coe_to_fun (normed_space.dual 𝕜 E)

source

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

source

@[instance]

def normed_space.inhabited (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (E : Type u_2) [normed_group E] [normed_space 𝕜 E] :

inhabited (normed_space.dual 𝕜 E)

Equations

normed_space.inhabited 𝕜 E = {default := 0}

source

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

normed_space.inclusion_in_double_dual' 𝕜 E x = {to_fun := λ (f : normed_space.dual 𝕜 E), ⇑f x, map_add' := _, map_smul' := _}.mk_continuous ∥x∥ _

source

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

⇑(normed_space.inclusion_in_double_dual' 𝕜 E x) f = ⇑f x

source

theorem normed_space.double_dual_bound (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (E : Type u_2) [normed_group E] [normed_space 𝕜 E] (x : E) :

∥normed_space.inclusion_in_double_dual' 𝕜 E x∥ ≤ ∥x∥

source

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

normed_space.inclusion_in_double_dual 𝕜 E = {to_fun := λ (x : E), normed_space.inclusion_in_double_dual' 𝕜 E x, map_add' := _, map_smul' := _}.mk_continuous 1 _

source

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.

source

theorem normed_space.inclusion_in_double_dual_isometry {𝕜 : Type v} [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜] [has_exists_extension_norm_eq 𝕜] {E : Type u} [normed_group E] [normed_space 𝕜 E] (x : E) :

∥⇑(normed_space.inclusion_in_double_dual 𝕜 E) x∥ = ∥x∥

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