# mathlibdocumentation

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) (E : Type u_2) [ E] :
@[instance]
def normed_space.dual.semi_normed_space (𝕜 : Type u_1) (E : Type u_2) [ E] :
def normed_space.dual (𝕜 : Type u_1) (E : Type u_2) [ E] :
Type (max u_2 u_1)

The topological dual of a seminormed space E.

Equations
@[instance]
def normed_space.dual.semi_normed_group (𝕜 : Type u_1) (E : Type u_2) [ E] :
@[instance]
def normed_space.dual.has_coe_to_fun (𝕜 : Type u_1) (E : Type u_2) [ E] :
(λ (_x : , E → 𝕜)
Equations
@[instance]
def normed_space.dual.normed_group (𝕜 : Type u_1) (F : Type u_3) [normed_group F] [ F] :
Equations
@[instance]
def normed_space.dual.normed_space (𝕜 : Type u_1) (F : Type u_3) [normed_group F] [ F] :
F)
Equations
def normed_space.inclusion_in_double_dual (𝕜 : Type u_1) (E : Type u_2) [ E] :
E →L[𝕜]

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

Equations
@[simp]
theorem normed_space.dual_def (𝕜 : Type u_1) (E : Type u_2) [ E] (x : E) (f : E) :
f = f x
theorem normed_space.inclusion_in_double_dual_norm_eq (𝕜 : Type u_1) (E : Type u_2) [ E] :
theorem normed_space.inclusion_in_double_dual_norm_le (𝕜 : Type u_1) (E : Type u_2) [ E] :
theorem normed_space.double_dual_bound (𝕜 : Type u_1) (E : Type u_2) [ E] (x : E) :
theorem normed_space.norm_le_dual_bound (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [ E] (x : E) {M : } (hMp : 0 M) (hM : ∀ (f : , 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] [ E] {x : E} (h : ∀ (f : , 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] [ E] (x : E) :
x = 0 ∀ (g : , g x = 0
theorem normed_space.eq_iff_forall_dual_eq (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [ E] {x y : E} :
x = y ∀ (g : , g x = g y
def normed_space.inclusion_in_double_dual_li (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [ E] :

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

Equations