The Gelfand triple V ↪ H ↪ V*

Let ι : V →L[ℝ] H be a continuous linear map from a real seminormed space V into a real inner product space H, which need only be seminormed. Pairing with H through ι gives the continuous linear map

ι.gelfandDual : H →L[ℝ] StrongDual ℝ V, h ↦ (x ↦ ⟪h, ι x⟫).

When H is normed and ι is injective with dense range, V ↪ H ↪ V* is a Gelfand triple (also called an evolution triple, with H the pivot space): ι.gelfandDual is then injective as well (ContinuousLinearMap.gelfandDual_injective), so H sits inside V*, and the pairing of V* with V restricts on H × V to the inner product of H. The standard example is H¹₀(Ω) ↪ L²(Ω) ↪ H⁻¹(Ω). Evolution equations u' + A u = f are posed in such a triple: the solution takes values in V, while its time derivative takes values in V*.

The composite ι.gelfandDual ∘ ι : V →L[ℝ] StrongDual ℝ V is the symmetric bilinear form (x, y) ↦ ⟪ι x, ι y⟫ (ContinuousLinearMap.flip_gelfandDual_comp).

Main declarations

• ContinuousLinearMap.gelfandDual: the map H → V*, h ↦ ⟪h, ι ·⟫.
• ContinuousLinearMap.gelfandDual_apply: its defining formula.
• ContinuousLinearMap.norm_gelfandDual: its norm is ‖ι‖.
• ContinuousLinearMap.gelfandDual_injective: for normed H, it is injective when ι has dense range.
• ContinuousLinearMap.flip_gelfandDual_comp: the form ⟪ι x, ι y⟫ on V is symmetric.
• ContinuousLinearMap.gelfandDual_comp_injective_iff: for normed H, the composite V → V* is injective exactly when ι is.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §5.9.2 and §7.1.
• E. Zeidler, Nonlinear Functional Analysis and its Applications II/A, Chapter 23.

noncomputable def ContinuousLinearMap.gelfandDual {V : Type u_1} {H : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [SeminormedAddCommGroup H] [InnerProductSpace ℝ H] (ι : V →L[ℝ] H) : H →L[ℝ] StrongDual ℝ V

The map H → V*, h ↦ (x ↦ ⟪h, ι x⟫), induced by a continuous linear map ι : V →L[ℝ] H into a real inner product space. When H is normed and ι is injective with dense range, this is the second embedding of the Gelfand triple V ↪ H ↪ V*.

@[simp]

theorem ContinuousLinearMap.gelfandDual_apply {V : Type u_1} {H : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [SeminormedAddCommGroup H] [InnerProductSpace ℝ H] (ι : V →L[ℝ] H) (h : H) (x : V) : (ι.gelfandDual h) x = inner ℝ h (ι x)

The defining formula of ContinuousLinearMap.gelfandDual.

@[simp]

theorem ContinuousLinearMap.norm_gelfandDual {V : Type u_1} {H : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [SeminormedAddCommGroup H] [InnerProductSpace ℝ H] (ι : V →L[ℝ] H) : ‖ι.gelfandDual‖ = ‖ι‖

The map H → V* of a Gelfand triple has the same norm as ι.

@[simp]

theorem ContinuousLinearMap.flip_gelfandDual_comp {V : Type u_1} {H : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [SeminormedAddCommGroup H] [InnerProductSpace ℝ H] (ι : V →L[ℝ] H) : (ι.gelfandDual ∘SL ι).flip = ι.gelfandDual ∘SL ι

The bilinear form (x, y) ↦ ⟪ι x, ι y⟫ that the composite V → H → V* defines on V is symmetric.

theorem ContinuousLinearMap.gelfandDual_injective {V : Type u_1} {H : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ι : V →L[ℝ] H) (hι : DenseRange ⇑ι) : Function.Injective ⇑ι.gelfandDual

If ι has dense range, the map H → V* is injective: an element of H orthogonal to the dense subspace ι(V) is zero. Together with an injective ι, this makes V ↪ H ↪ V* a chain of continuous embeddings.

theorem ContinuousLinearMap.gelfandDual_comp_injective_iff {V : Type u_1} {H : Type u_2} [SeminormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ι : V →L[ℝ] H) : Function.Injective ⇑(ι.gelfandDual ∘SL ι) ↔ Function.Injective ⇑ι

The composite ι.gelfandDual ∘ ι : V → V* is injective exactly when ι is: testing ι.gelfandDual (ι x) on x returns ‖ι x‖².