# mathlib3documentation

analysis.inner_product_space.dual

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

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 E using to_dual.

## Tags #

noncomputable def inner_product_space.to_dual_map (π : Type u_1) (E : Type u_2) [is_R_or_C π] [ 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 π] [ E] {x y : E} :
β(β E) x) y =
theorem inner_product_space.innerSL_norm (π : Type u_1) {E : Type u_2} [is_R_or_C π] [ E] [nontrivial E] :
theorem inner_product_space.ext_inner_left_basis {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {ΞΉ : Type u_3} {x y : E} (b : basis ΞΉ π E) (h : β (i : ΞΉ), has_inner.inner (βb i) x = has_inner.inner (βb i) y) :
x = y
theorem inner_product_space.ext_inner_right_basis {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {ΞΉ : Type u_3} {x y : E} (b : basis ΞΉ π E) (h : β (i : ΞΉ), (βb i) = (βb i)) :
x = y
noncomputable def inner_product_space.to_dual (π : Type u_1) (E : Type u_2) [is_R_or_C π] [ 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 π] [ E] {x y : E} :
β(β E) x) y =
@[simp]
theorem inner_product_space.to_dual_symm_apply {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ E] {x : E} {y : E} :
noncomputable def inner_product_space.continuous_linear_map_of_bilin {π : Type u_1} {E : Type u_2} [is_R_or_C π] [ 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β[π] normed_space.dual π E and dualizing the result using to_dual.

Equations
@[simp]
theorem inner_product_space.continuous_linear_map_of_bilin_apply (π : Type u_1) {E : Type u_2} [is_R_or_C π] [ E] (B : E βLβ[π] E βL[π] π) (v w : E) :
theorem inner_product_space.unique_continuous_linear_map_of_bilin (π : Type u_1) {E : Type u_2} [is_R_or_C π] [ E] (B : E βLβ[π] E βL[π] π) {v f : E} (is_lax_milgram : β (w : E), = β(βB v) w) :