mathlib documentation

analysis.normed_space.dual

The topological dual of a normed space #

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

For base field 𝕜 = ℝ or 𝕜 = ℂ, this map is actually an isometric embedding; we provide a version normed_space.inclusion_in_double_dual_li of the map which is of type a bundled linear isometric embedding, E →ₗᵢ[𝕜] (dual 𝕜 (dual 𝕜 E)).

Since a lot of elementary properties don't require eq_of_dist_eq_zero we start setting up the theory for semi_normed_space and we specialize to normed_space when needed.

Tags #

dual

@[instance]

def normed_space.dual.inhabited (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (E : Type u_2) [semi_normed_group E] [semi_normed_space 𝕜 E] :

inhabited (normed_space.dual 𝕜 E)

@[instance]

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

semi_normed_space 𝕜 (normed_space.dual 𝕜 E)

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

Type (max u_2 u_1)

The topological dual of a seminormed space E.

Equations

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

@[instance]

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

semi_normed_group (normed_space.dual 𝕜 E)

@[instance]

def normed_space.dual.has_coe_to_fun (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (E : Type u_2) [semi_normed_group E] [semi_normed_space 𝕜 E] :

has_coe_to_fun (normed_space.dual 𝕜 E) (λ (_x : normed_space.dual 𝕜 E), E → 𝕜)

Equations

normed_space.dual.has_coe_to_fun 𝕜 E = continuous_linear_map.to_fun

@[instance]

def normed_space.dual.normed_group (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (F : Type u_3) [normed_group F] [normed_space 𝕜 F] :

normed_group (normed_space.dual 𝕜 F)

Equations

normed_space.dual.normed_group 𝕜 F = continuous_linear_map.to_normed_group

@[instance]

def normed_space.dual.normed_space (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (F : Type u_3) [normed_group F] [normed_space 𝕜 F] :

normed_space 𝕜 (normed_space.dual 𝕜 F)

Equations

normed_space.dual.normed_space 𝕜 F = continuous_linear_map.to_normed_space

def normed_space.inclusion_in_double_dual (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (E : Type u_2) [semi_normed_group E] [semi_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 = continuous_linear_map.apply 𝕜 𝕜

@[simp]

theorem normed_space.dual_def (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (E : Type u_2) [semi_normed_group E] [semi_normed_space 𝕜 E] (x : E) (f : normed_space.dual 𝕜 E) :

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

theorem normed_space.inclusion_in_double_dual_norm_eq (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (E : Type u_2) [semi_normed_group E] [semi_normed_space 𝕜 E] :

∥normed_space.inclusion_in_double_dual 𝕜 E∥ = ∥continuous_linear_map.id 𝕜 (normed_space.dual 𝕜 E)∥

theorem normed_space.inclusion_in_double_dual_norm_le (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] (E : Type u_2) [semi_normed_group E] [semi_normed_space 𝕜 E] :

∥normed_space.inclusion_in_double_dual 𝕜 E∥ ≤ 1

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

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

theorem normed_space.norm_le_dual_bound (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [normed_space 𝕜 E] (x : E) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (f : normed_space.dual 𝕜 E), ∥⇑f x∥ ≤ M * ∥f∥) :

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

theorem normed_space.eq_zero_of_forall_dual_eq_zero (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [normed_space 𝕜 E] {x : E} (h : ∀ (f : normed_space.dual 𝕜 E), ⇑f x = 0) :

x = 0

theorem normed_space.eq_zero_iff_forall_dual_eq_zero (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [normed_space 𝕜 E] (x : E) :

x = 0 ↔ ∀ (g : normed_space.dual 𝕜 E), ⇑g x = 0

theorem normed_space.eq_iff_forall_dual_eq (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [normed_space 𝕜 E] {x y : E} :

x = y ↔ ∀ (g : normed_space.dual 𝕜 E), ⇑g x = ⇑g y

def normed_space.inclusion_in_double_dual_li (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [normed_space 𝕜 E] :

E →ₗᵢ[𝕜] normed_space.dual 𝕜 (normed_space.dual 𝕜 E)

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

Equations

normed_space.inclusion_in_double_dual_li 𝕜 = {to_linear_map := (normed_space.inclusion_in_double_dual 𝕜 E).to_linear_map, norm_map' := _}