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

dual, Fréchet-Riesz

def InnerProductSpace.toDualMap (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →ₗᵢ⋆[𝕜] NormedSpace.Dual 𝕜 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

• InnerProductSpace.toDualMap 𝕜 E = { toLinearMap := ↑(innerSL 𝕜), norm_map' := ⋯ }

@[simp]

theorem InnerProductSpace.toDualMap_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} : ((toDualMap 𝕜 E) x) y = inner 𝕜 x y

theorem InnerProductSpace.nullSubmodule_le_ker_toDualMap_right (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : nullSubmodule 𝕜 E ≤ LinearMap.ker ((toDualMap 𝕜 E) x)

For each x : E, the kernel of ⟪x, ⬝⟫ includes the null space.

theorem InnerProductSpace.nullSubmodule_le_ker_toDualMap_left (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : nullSubmodule 𝕜 E ≤ LinearMap.ker (toDualMap 𝕜 E)

The kernel of the map x ↦ ⟪·, x⟫ includes the null space.

theorem InnerProductSpace.innerSL_norm (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Nontrivial E] : ‖innerSL 𝕜‖ = 1

theorem InnerProductSpace.ext_inner_left_basis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} {x y : E} (b : Basis ι 𝕜 E) (h : ∀ (i : ι), inner 𝕜 (b i) x = inner 𝕜 (b i) y) : x = y

theorem InnerProductSpace.ext_inner_right_basis {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} {x y : E} (b : Basis ι 𝕜 E) (h : ∀ (i : ι), inner 𝕜 x (b i) = inner 𝕜 y (b i)) : x = y

def InnerProductSpace.toDual (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : E ≃ₗᵢ⋆[𝕜] NormedSpace.Dual 𝕜 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

• InnerProductSpace.toDual 𝕜 E = LinearIsometryEquiv.ofSurjective (InnerProductSpace.toDualMap 𝕜 E) ⋯

@[simp]

theorem InnerProductSpace.toDual_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {x y : E} : ((toDual 𝕜 E) x) y = inner 𝕜 x y

@[simp]

theorem InnerProductSpace.toDual_symm_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {x : E} {y : NormedSpace.Dual 𝕜 E} : inner 𝕜 ((toDual 𝕜 E).symm y) x = y x

def InnerProductSpace.continuousLinearMapOfBilin {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace 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

• InnerProductSpace.continuousLinearMapOfBilin B = (↑(InnerProductSpace.toDual 𝕜 E).symm.toContinuousLinearEquiv).comp B

@[simp]

theorem InnerProductSpace.continuousLinearMapOfBilin_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) (v w : E) : inner 𝕜 ((continuousLinearMapOfBilin B) v) w = (B v) w

theorem InnerProductSpace.unique_continuousLinearMapOfBilin {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) {v f : E} (is_lax_milgram : ∀ (w : E), inner 𝕜 f w = (B v) w) : f = (continuousLinearMapOfBilin B) v