Documentation

Mathlib.Analysis.InnerProductSpace.Dual

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] [EinsiedlerWard2017]

Tags #

dual, Fréchet-Riesz

def InnerProductSpace.toDualMap (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

E →ₗᵢ⋆[𝕜] StrongDual 𝕜 E

An element x of an inner product space E induces an element of the strong dual space StrongDual 𝕜 E, the map fun y => ⟪x, y⟫; moreover this operation is a conjugate-linear isometric embedding of E into StrongDual 𝕜 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' := ⋯ }

Instances For

@[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

@[simp]

theorem innerSL_inj {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} :

(innerSL 𝕜) x = (innerSL 𝕜) y ↔ 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 : Module.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 : Module.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 ≃ₗᵢ⋆[𝕜] StrongDual 𝕜 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) ⋯

Instances For

@[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 : StrongDual 𝕜 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⋆[𝕜] StrongDual 𝕜 E and dualizing the result using toDual.

Equations

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

Instances For

@[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

instance InnerProductSpace.instIsContPerfPairRealInnerₗOfCompleteSpace (E : Type u_2) [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace ℝ E] :

(innerₗ E).IsContPerfPair