# 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 #

def InnerProductSpace.toDualMap (π : Type u_1) (E : Type u_2) [RCLike π] [InnerProductSpace π 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
• = let __src := innerSL π; { toLinearMap := β__src, norm_map' := β― }
Instances For
@[simp]
theorem InnerProductSpace.toDualMap_apply (π : Type u_1) {E : Type u_2} [RCLike π] [InnerProductSpace π E] {x : E} {y : E} :
(() x) y = βͺx, yβ«_π
theorem InnerProductSpace.innerSL_norm (π : Type u_1) {E : Type u_2} [RCLike π] [InnerProductSpace π E] [] :
theorem InnerProductSpace.ext_inner_left_basis {π : Type u_1} {E : Type u_2} [RCLike π] [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 π] [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 π] [InnerProductSpace π 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
Instances For
@[simp]
theorem InnerProductSpace.toDual_apply {π : Type u_1} {E : Type u_2} [RCLike π] [InnerProductSpace π E] [] {x : E} {y : E} :
(() x) y = βͺx, yβ«_π
@[simp]
theorem InnerProductSpace.toDual_symm_apply {π : Type u_1} {E : Type u_2} [RCLike π] [InnerProductSpace π E] [] {x : E} {y : NormedSpace.Dual π E} :
βͺ().symm y, xβ«_π = y x
def InnerProductSpace.continuousLinearMapOfBilin {π : Type u_1} {E : Type u_2} [RCLike π] [InnerProductSpace π 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
• = (β().symm.toContinuousLinearEquiv).comp B
Instances For
@[simp]
theorem InnerProductSpace.continuousLinearMapOfBilin_apply {π : Type u_1} {E : Type u_2} [RCLike π] [InnerProductSpace π E] [] (B : E βLβ[π] E βL[π] π) (v : E) (w : E) :
βͺ, wβ«_π = (B v) w
theorem InnerProductSpace.unique_continuousLinearMapOfBilin {π : Type u_1} {E : Type u_2} [RCLike π] [InnerProductSpace π E] [] (B : E βLβ[π] E βL[π] π) {v : E} {f : E} (is_lax_milgram : β (w : E), βͺf, wβ«_π = (B v) w) :