mathlib documentation

analysis.inner_product_space.dual

The FrΓ©chet-Riesz representation theorem #

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.

References #

Tags #

dual, FrΓ©chet-Riesz

noncomputable def inner_product_space.to_dual_map (π•œ : Type u_1) (E : Type u_2) [is_R_or_C π•œ] [inner_product_space π•œ 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 π•œ] [inner_product_space π•œ E] {x y : E} :
theorem inner_product_space.innerSL_norm (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [inner_product_space π•œ E] [nontrivial E] :
theorem inner_product_space.ext_inner_left (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [inner_product_space π•œ E] {x y : E} (h : βˆ€ (v : E), has_inner.inner v x = has_inner.inner v y) :
x = y
theorem inner_product_space.ext_inner_right (π•œ : Type u_1) {E : Type u_2} [is_R_or_C π•œ] [inner_product_space π•œ E] {x y : E} (h : βˆ€ (v : E), has_inner.inner x v = has_inner.inner y v) :
x = y
theorem inner_product_space.ext_inner_left_basis {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [inner_product_space π•œ 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 π•œ] [inner_product_space π•œ E] {ΞΉ : Type u_3} {x y : E} (b : basis ΞΉ π•œ E) (h : βˆ€ (i : ΞΉ), has_inner.inner x (⇑b i) = has_inner.inner y (⇑b i)) :
x = y
noncomputable def inner_product_space.to_dual (π•œ : Type u_1) (E : Type u_2) [is_R_or_C π•œ] [inner_product_space π•œ E] [complete_space 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 π•œ] [inner_product_space π•œ E] [complete_space E] {x y : E} :
@[simp]
theorem inner_product_space.to_dual_symm_apply {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [inner_product_space π•œ E] [complete_space E] {x : E} {y : normed_space.dual π•œ E} :
noncomputable def inner_product_space.continuous_linear_map_of_bilin {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [inner_product_space π•œ E] [complete_space 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 π•œ] [inner_product_space π•œ E] [complete_space 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 π•œ] [inner_product_space π•œ E] [complete_space E] (B : E β†’L⋆[π•œ] E β†’L[π•œ] π•œ) {v f : E} (is_lax_milgram : βˆ€ (w : E), has_inner.inner f w = ⇑(⇑B v) w) :