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 #

Tags #

dual, Fréchet-Riesz

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

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

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

    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

    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
    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 : 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
      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) :