The Fréchet-Riesz representation theorem #
We consider an inner product space E
over 𝕜
, which is either ℝ
or ℂ
. We define
toDualMap
, a conjugate-linear isometric embedding of E
into its dual, which maps an element
x
of the space to fun y => ⟪x, y⟫
.
Under the hypothesis of completeness (i.e., for Hilbert spaces), we upgrade this to toDual
, a
conjugate-linear isometric equivalence of E
onto its dual; that is, we establish the
surjectivity of toDualMap
. This is the Fréchet-Riesz representation theorem: every element of
the dual of a Hilbert space E
has the form fun u => ⟪x, u⟫
for some x : E
.
For a bounded sesquilinear form B : E →L⋆[𝕜] E →L[𝕜] 𝕜
,
we define a map InnerProductSpace.continuousLinearMapOfBilin B : E →L[𝕜] E
,
given by substituting E →L[𝕜] 𝕜
with E
using toDual
.
References #
- [M. Einsiedler and T. Ward, Functional Analysis, Spectral Theory, and Applications] [EW17]
Tags #
dual, Fréchet-Riesz
An element x
of an inner product space E
induces an element of the dual space Dual 𝕜 E
,
the map fun 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 toDual
.
Equations
- InnerProductSpace.toDualMap 𝕜 E = { toLinearMap := ↑(innerSL 𝕜), norm_map' := ⋯ }
Instances For
For each x : E
, the kernel of ⟪x, ⬝⟫
includes the null space.
The kernel of the map x ↦ ⟪·, x⟫
includes the null space.
Fréchet-Riesz representation: any ℓ
in the dual of a Hilbert space E
is of the form
fun u => ⟪y, u⟫
for some y : E
, i.e. toDualMap
is surjective.
Equations
Instances For
Maps a bounded sesquilinear form to its continuous linear map,
given by interpreting the form as a map B : E →L⋆[𝕜] NormedSpace.Dual 𝕜 E
and dualizing the result using toDual
.