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.

References #

M. Einsiedler and T. Ward, Functional Analysis, Spectral Theory, and Applications

Tags #

dual, Fréchet-Riesz

source

noncomputable def inner_product_space.to_dual_map (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] :

E →ₗᵢ⋆[𝕜] normed_space.dual 𝕜 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

inner_product_space.to_dual_map 𝕜 E = {to_linear_map := (innerSL 𝕜).to_linear_map, norm_map' := _}

source

@[simp]

theorem inner_product_space.to_dual_map_apply (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {x y : E} :

⇑(⇑(inner_product_space.to_dual_map 𝕜 E) x) y = has_inner.inner x y

source

theorem inner_product_space.innerSL_norm (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [nontrivial E] :

‖innerSL 𝕜‖ = 1

source

theorem inner_product_space.ext_inner_left_basis {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [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

source

theorem inner_product_space.ext_inner_right_basis {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [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

source

noncomputable def inner_product_space.to_dual (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] :

E ≃ₗᵢ⋆[𝕜] normed_space.dual 𝕜 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

inner_product_space.to_dual 𝕜 E = linear_isometry_equiv.of_surjective (inner_product_space.to_dual_map 𝕜 E) _

source

@[simp]

theorem inner_product_space.to_dual_apply {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] {x y : E} :

⇑(⇑(inner_product_space.to_dual 𝕜 E) x) y = has_inner.inner x y

source

@[simp]

theorem inner_product_space.to_dual_symm_apply {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] {x : E} {y : normed_space.dual 𝕜 E} :

has_inner.inner (⇑((inner_product_space.to_dual 𝕜 E).symm) y) x = ⇑y x

source

noncomputable def inner_product_space.continuous_linear_map_of_bilin {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [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

inner_product_space.continuous_linear_map_of_bilin B = (inner_product_space.to_dual 𝕜 E).symm.to_continuous_linear_equiv.to_continuous_linear_map.comp B

source

@[simp]

theorem inner_product_space.continuous_linear_map_of_bilin_apply (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) (v w : E) :

has_inner.inner (⇑(inner_product_space.continuous_linear_map_of_bilin B) v) w = ⇑(⇑B v) w

source

theorem inner_product_space.unique_continuous_linear_map_of_bilin (𝕜 : Type u_1) {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [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) :

f = ⇑(inner_product_space.continuous_linear_map_of_bilin B) v