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 π•œ 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.

References

Tags

dual, FrΓ©chet-Riesz

@[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.dual.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] (x : 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} [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.inclusion_in_double_dual_isometry {π•œ : Type v} [is_R_or_C π•œ] {E : Type u} [normed_group E] [normed_space π•œ 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 π•œ] [inner_product_space π•œ 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 π•œ] [inner_product_space π•œ E] {x y : E} :

@[simp]
theorem inner_product_space.norm_to_dual'_apply (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [inner_product_space π•œ 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 π•œ] [inner_product_space π•œ E] :

theorem inner_product_space.to_dual'_surjective (π•œ : Type u_1) (E : Type u_2) [is_R_or_C π•œ] [inner_product_space π•œ E] [complete_space 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.

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]

In an inner product space, the norm of the dual of a vector x is βˆ₯xβˆ₯

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.

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

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
theorem inner_product_space.to_dual_eq_iff_eq' {F : Type u_1} [inner_product_space ℝ F] [complete_space F] {x x' : F} :
(βˆ€ (y : F), inner x y = inner x' y) ↔ x = x'

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