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] [EinsiedlerWard2017]

Tags

dual, Fréchet-Riesz

def InnerProductSpace.toDualMap (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →ₗᵢ⋆[𝕜] NormedSpace.Dual 𝕜 E

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 = let __src := innerSL 𝕜; { toLinearMap := ↑__src, norm_map' := ⋯ }

@[simp]

theorem InnerProductSpace.toDualMap_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {y : E} : ((InnerProductSpace.toDualMap 𝕜 E) x) y = ⟪x, y⟫_𝕜

theorem InnerProductSpace.innerSL_norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Nontrivial E] : ‖innerSL 𝕜‖ = 1

theorem InnerProductSpace.ext_inner_left_basis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} {x : E} {y : E} (b : Basis ι 𝕜 E) (h : ∀ (i : ι), ⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜) : x = y

theorem InnerProductSpace.ext_inner_right_basis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} {x : E} {y : E} (b : Basis ι 𝕜 E) (h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜) : x = y

def InnerProductSpace.toDual (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : E ≃ₗᵢ⋆[𝕜] NormedSpace.Dual 𝕜 E

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

• InnerProductSpace.toDual 𝕜 E = LinearIsometryEquiv.ofSurjective (InnerProductSpace.toDualMap 𝕜 E) ⋯

@[simp]

theorem InnerProductSpace.toDual_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {x : E} {y : E} : ((InnerProductSpace.toDual 𝕜 E) x) y = ⟪x, y⟫_𝕜

@[simp]

theorem InnerProductSpace.toDual_symm_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {x : E} {y : NormedSpace.Dual 𝕜 E} : ⟪(InnerProductSpace.toDual 𝕜 E).symm y, x⟫_𝕜 = y x

def InnerProductSpace.continuousLinearMapOfBilin {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) : E →L[𝕜] E

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.

Equations

• InnerProductSpace.continuousLinearMapOfBilin B = (↑(InnerProductSpace.toDual 𝕜 E).symm.toContinuousLinearEquiv).comp B

@[simp]

theorem InnerProductSpace.continuousLinearMapOfBilin_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) (v : E) (w : E) : ⟪(InnerProductSpace.continuousLinearMapOfBilin B) v, w⟫_𝕜 = (B v) w

theorem InnerProductSpace.unique_continuousLinearMapOfBilin {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) {v : E} {f : E} (is_lax_milgram : ∀ (w : E), ⟪f, w⟫_𝕜 = (B v) w) : f = (InnerProductSpace.continuousLinearMapOfBilin B) v