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

def InnerProductSpace.toDualMap (π•œ : Type u_1) (E : Type u_2) [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ 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
    @[simp]
    theorem InnerProductSpace.toDualMap_apply (π•œ : Type u_1) {E : Type u_2} [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ E] {x : E} {y : E} :
    ((InnerProductSpace.toDualMap π•œ E) x) y = βŸͺx, y⟫_π•œ
    theorem InnerProductSpace.innerSL_norm (π•œ : Type u_1) {E : Type u_2} [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ E] [Nontrivial E] :
    theorem InnerProductSpace.ext_inner_left_basis {π•œ : Type u_1} {E : Type u_2} [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ E] {ΞΉ : Type u_3} {x : E} {y : E} (b : Basis ΞΉ π•œ E) (h : βˆ€ (i : ΞΉ), βŸͺb i, x⟫_π•œ = βŸͺ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 : E} {y : E} (b : Basis ΞΉ π•œ E) (h : βˆ€ (i : ΞΉ), βŸͺx, b i⟫_π•œ = βŸͺy, b i⟫_π•œ) :
    x = y
    def InnerProductSpace.toDual (π•œ : Type u_1) (E : Type u_2) [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ E] [CompleteSpace 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
      @[simp]
      theorem InnerProductSpace.toDual_apply {π•œ : Type u_1} {E : Type u_2} [RCLike π•œ] [NormedAddCommGroup E] [InnerProductSpace π•œ E] [CompleteSpace E] {x : E} {y : E} :
      ((InnerProductSpace.toDual π•œ E) x) y = βŸͺ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} :
      βŸͺ(InnerProductSpace.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 : E) (w : E) :
        βŸͺ(InnerProductSpace.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 : E} {f : E} (is_lax_milgram : βˆ€ (w : E), βŸͺf, w⟫_π•œ = (B v) w) :