mathlib documentation

analysis.inner_product_space.dual

The Fréchet-Riesz representation theorem #

We consider an inner product space E over 𝕜, which is either or . We define to_dual_map, a conjugate-linear isometric embedding of E into its dual, which maps an element x of the space to λ y, ⟪x, y⟫.

Under the hypothesis of completeness (i.e., for Hilbert spaces), we upgrade this to to_dual, a conjugate-linear isometric equivalence of E onto its dual; that is, we establish the surjectivity of to_dual_map. This is the Fréchet-Riesz representation theorem: every element of the dual of a Hilbert space E has the form λ u, ⟪x, u⟫ for some x : E.

References #

Tags #

dual, Fréchet-Riesz

noncomputable def inner_product_space.to_dual_map (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] :

An element x of an inner product space E induces an element of the dual space dual 𝕜 E, the map λ y, ⟪x, y⟫; moreover this operation is a conjugate-linear isometric embedding of E into dual 𝕜 E. If E is complete, this operation is surjective, hence a conjugate-linear isometric equivalence; see to_dual.

Equations
@[simp]
theorem inner_product_space.to_dual_map_apply (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] {x y : E} :
noncomputable def inner_product_space.to_dual (𝕜 : 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_map is surjective.

Equations
@[simp]
theorem inner_product_space.to_dual_apply (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] {x y : E} :
@[simp]
theorem inner_product_space.to_dual_symm_apply (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] {x : E} {y : normed_space.dual 𝕜 E} :