# mathlibdocumentation

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 𝕜 with [is_R_or_C 𝕜], this map is an isometry.

We then consider inner product spaces, with base field over ℝ (the corresponding results for ℂ will require the definition of conjugate-linear maps). We define to_dual_map, a continuous linear map from E to its dual, which maps an element x of the space to λ y, ⟪x, y⟫. We check (to_dual_map_isometry) that this map is an isometry onto its image, and particular is injective. We also define to_dual' as the function taking taking a vector to its dual for a base field 𝕜 with [is_R_or_C 𝕜]; this is a function and not a linear map.

Finally, under the hypothesis of completeness (i.e., for Hilbert spaces), we prove the Fréchet-Riesz representation (to_dual_map_eq_top), which states the surjectivity: every element of the dual of a Hilbert space E has the form λ u, ⟪x, u⟫ for some x : E. This permits the map to_dual_map to be upgraded to an (isometric) continuous linear equivalence, to_dual, between a Hilbert space and its dual.

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, Fréchet-Riesz

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

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

Equations
@[simp]
theorem normed_space.dual_def (𝕜 : Type u_1) (E : Type u_2) [ E] (x : E) (f : E) :
= f x
theorem normed_space.double_dual_bound (𝕜 : Type u_1) (E : Type u_2) [ E] (x : E) :
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
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
theorem normed_space.inclusion_in_double_dual_isometry (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [ E] (x : E) :

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

def inner_product_space.to_dual' (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] :
E →+

Given some x in an inner product space, we can define its dual as the continuous linear map λ y, ⟪x, y⟫. Consider using to_dual or to_dual_map instead in the real case.

Equations
@[simp]
theorem inner_product_space.to_dual'_apply (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] {x y : E} :
y = y
@[simp]
theorem inner_product_space.norm_to_dual'_apply (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [ E] (x : E) :

In an inner product space, the norm of the dual of a vector x is ∥x∥

theorem inner_product_space.to_dual'_isometry (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [ E] :
theorem inner_product_space.to_dual'_surjective (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [ E]  :

Fréchet-Riesz representation: any ℓ in the dual of a Hilbert space E is of the form λ u, ⟪y, u⟫ for some y : E, i.e. to_dual' is surjective.

def inner_product_space.to_dual_map {F : Type u_1}  :

In a real inner product space F, the function that takes a vector x in F to its dual λ y, ⟪x, y⟫ is a continuous linear map. If the space is complete (i.e. is a Hilbert space), consider using to_dual instead.

Equations
@[simp]
theorem inner_product_space.to_dual_map_apply {F : Type u_1} {x y : F} :
= y
@[simp]
theorem inner_product_space.norm_to_dual_map_apply {F : Type u_1} (x : F) :

In an inner product space, the norm of the dual of a vector x is ∥x∥

@[simp]
theorem inner_product_space.ker_to_dual_map {F : Type u_1}  :
@[simp]
theorem inner_product_space.to_dual_map_eq_iff_eq {F : Type u_1} {x y : F} :
theorem inner_product_space.range_to_dual_map {F : Type u_1}  :

Fréchet-Riesz representation: any ℓ in the dual of a real Hilbert space F is of the form λ u, ⟪y, u⟫ for some y in F. See inner_product_space.to_dual for the continuous linear equivalence thus induced.

def inner_product_space.to_dual {F : Type u_1}  :

Fréchet-Riesz representation: If F is a Hilbert space, the function that takes a vector in F to its dual is a continuous linear equivalence.

Equations
def inner_product_space.isometric.to_dual {F : Type u_1}  :

Fréchet-Riesz representation: If F is a Hilbert space, the function that takes a vector in F to its dual is an isometry.

Equations
@[simp]
theorem inner_product_space.to_dual_apply {F : Type u_1} {x y : F} :
= y
@[simp]
theorem inner_product_space.to_dual_eq_iff_eq {F : Type u_1} {x y : F} :
theorem inner_product_space.to_dual_eq_iff_eq' {F : Type u_1} {x x' : F} :
(∀ (y : F), y = inner x' y) x = x'
@[simp]
theorem inner_product_space.norm_to_dual_apply {F : Type u_1} (x : F) :
theorem inner_product_space.norm_to_dual_symm_apply {F : Type u_1} (ℓ : F) :

In a Hilbert space, the norm of a vector in the dual space is the norm of its corresponding primal vector.