The Fréchet-Riesz representation theorem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We consider an inner product space
𝕜, which is either
ℂ. 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
conjugate-linear isometric equivalence of
E onto its dual; that is, we establish the
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.
For a bounded sesquilinear form
B : E →L⋆[𝕜] E →L[𝕜] 𝕜,
we define a map
inner_product_space.continuous_linear_map_of_bilin B : E →L[𝕜] E,
given by substituting
E →L[𝕜] 𝕜 with
x of an inner product space
E induces an element of the dual space
dual 𝕜 E,
λ y, ⟪x, y⟫; moreover this operation is a conjugate-linear isometric embedding of
dual 𝕜 E.
E is complete, this operation is surjective, hence a conjugate-linear isometric equivalence;
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.
Maps a bounded sesquilinear form to its continuous linear map,
given by interpreting the form as a map
B : E →L⋆[𝕜] normed_space.dual 𝕜 E
and dualizing the result using