# mathlibdocumentation

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.

## Tags #

dual, Fréchet-Riesz

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} :
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 : 𝕜 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 : 𝕜 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} :
( 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) :
= (B v) w
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) :