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

source
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
Instances For
    source
    @[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
    source
    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.

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

    source
    theorem InnerProductSpace.innerSL_norm (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Nontrivial E] :
    ‖innerSL 𝕜‖ = 1
    source
    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
    source
    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
    source
    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
    Instances For
      source
      @[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
      source
      @[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
      source
      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
        source
        @[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
        source
        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
        source
        instance InnerProductSpace.instIsContPerfPairRealInnerₗOfCompleteSpace (E : Type u_2) [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace ℝ E] :
        (innerₗ E).IsContPerfPair