Time-dependent functions in a Gelfand triple are continuous into the pivot space

Let V ↪ H ↪ V* be a Gelfand triple, given by a continuous linear map ι : V →L[ℝ] H into a real Hilbert space H (ContinuousLinearMap.gelfandDual). Let u ∈ L²(a, b; V), and suppose that u, viewed in V* through V → H → V*, has a weak time derivative u' ∈ L²(a, b; V*). Neither u nor ι ∘ u is assumed to have any continuity in time. This file proves:

• ι ∘ u agrees almost everywhere on (a, b) with a function w : ℝ → H continuous on [a, b] (TauCeti.HasWeakLineDerivOn.exists_continuousOn_ae_eq_of_gelfandDual);
• every such w satisfies the energy identity ‖w t‖² - ‖w s‖² = 2 ∫ₛᵗ u'(r)(u r) dr for all s, t ∈ [a, b] (TauCeti.HasWeakLineDerivOn.norm_sq_sub_norm_sq_eq_of_gelfandDual);
• two such functions satisfy the mixed integration-by-parts formula (TauCeti.HasWeakLineDerivOn.inner_sub_inner_eq_integral_of_gelfandDual);
• and the bound ‖w t‖² ≤ ⨍_{(a, b)} ‖ι u‖² + 2 ∫_{(a, b)} |u'(u)|, which controls sup_t ‖w t‖ by the norms of u in L²(a, b; V) and of u' in L²(a, b; V*) (TauCeti.HasWeakLineDerivOn.norm_sq_le_of_gelfandDual).

Together these are the analytic content of the embedding L²(a, b; V) ∩ H¹(a, b; V*) ↪ C([a, b]; H): a continuous representative exists, and its supremum norm is controlled by the norms of u and u'. They are stated for pointwise representatives u, u'; packaging the domain as a normed space and the representative as a bounded linear map is not done here.

This is the setting of linear parabolic equations: a weak solution of u' + A u = f lies in L²(0, T; H¹₀(Ω)) with u' ∈ L²(0, T; H⁻¹(Ω)), so it has a representative in C([0, T]; L²(Ω)), which gives meaning to the initial condition u(0) = u₀, and its energy identity yields uniqueness.

References

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

theorem TauCeti.HasWeakLineDerivOn.exists_continuousOn_ae_eq_of_gelfandDual {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : V →L[ℝ] H} {a b : ℝ} {u : ℝ → V} {u' : ℝ → StrongDual ℝ V} [CompleteSpace V] [CompleteSpace H] (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } (fun (t : ℝ) => ι.gelfandDual (ι (u t))) u' 1) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) (hu' : MeasureTheory.MemLp u' 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) : ∃ (w : ℝ → H), ContinuousOn w (Set.Icc a b) ∧ (fun (t : ℝ) => ι (u t)) =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] w

A time-dependent function in a Gelfand triple is continuous into the pivot space. Let ι : V →L[ℝ] H with H a Hilbert space, let u ∈ L²(a, b; V), and suppose that t ↦ ι.gelfandDual (ι (u t)) has weak derivative u' ∈ L²(a, b; V*) on (a, b). Then ι ∘ u agrees almost everywhere on (a, b) with a function continuous on [a, b].

theorem TauCeti.HasWeakLineDerivOn.norm_sq_sub_norm_sq_eq_of_gelfandDual {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : V →L[ℝ] H} {a b : ℝ} {u : ℝ → V} {u' : ℝ → StrongDual ℝ V} [CompleteSpace V] (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } (fun (t : ℝ) => ι.gelfandDual (ι (u t))) u' 1) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) (hu' : MeasureTheory.MemLp u' 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) {w : ℝ → H} (hw : ContinuousOn w (Set.Icc a b)) (hae : (fun (t : ℝ) => ι (u t)) =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] w) {s t : ℝ} (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) : ‖w t‖ ^ 2 - ‖w s‖ ^ 2 = 2 * ∫ (r : ℝ) in s..t, (u' r) (u r)

The energy identity in a Gelfand triple. Let u ∈ L²(a, b; V) be such that t ↦ ι.gelfandDual (ι (u t)) has weak derivative u' ∈ L²(a, b; V*) on (a, b), and let w be continuous on [a, b] and equal to ι ∘ u almost everywhere on (a, b). Then for all s, t ∈ [a, b], ‖w t‖² - ‖w s‖² = 2 ∫ₛᵗ u'(r)(u r) dr.

theorem TauCeti.HasWeakLineDerivOn.inner_sub_inner_eq_integral_of_gelfandDual {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : V →L[ℝ] H} {a b : ℝ} {u : ℝ → V} {u' : ℝ → StrongDual ℝ V} [CompleteSpace V] (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } (fun (t : ℝ) => ι.gelfandDual (ι (u t))) u' 1) {z : ℝ → V} {z' : ℝ → StrongDual ℝ V} (hz : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } (fun (t : ℝ) => ι.gelfandDual (ι (z t))) z' 1) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) (hu' : MeasureTheory.MemLp u' 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) (hzL : MeasureTheory.MemLp z 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) (hz' : MeasureTheory.MemLp z' 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) {w q : ℝ → H} (hw : ContinuousOn w (Set.Icc a b)) (hq : ContinuousOn q (Set.Icc a b)) (hae : (fun (t : ℝ) => ι (u t)) =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] w) (hzae : (fun (t : ℝ) => ι (z t)) =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] q) {s t : ℝ} (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) : inner ℝ (w t) (q t) - inner ℝ (w s) (q s) = ∫ (r : ℝ) in s..t, (u' r) (z r) + (z' r) (u r)

Integration by parts in a Gelfand triple. If u, z ∈ L²(a,b;V) have dual-valued weak time derivatives u', z' ∈ L²(a,b;V*), then their continuous pivot representatives w, q satisfy ⟪w t, q t⟫ - ⟪w s, q s⟫ = ∫ₛᵗ (u'(z) + z'(u)), including endpoint times. Neither injectivity nor dense range of the pivot map is required.

theorem TauCeti.HasWeakLineDerivOn.norm_sq_le_of_gelfandDual {V : Type u_1} {H : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : V →L[ℝ] H} {a b : ℝ} {u : ℝ → V} {u' : ℝ → StrongDual ℝ V} [CompleteSpace V] (h : HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } (fun (t : ℝ) => ι.gelfandDual (ι (u t))) u' 1) (hab : a < b) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) (hu' : MeasureTheory.MemLp u' 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) {w : ℝ → H} (hw : ContinuousOn w (Set.Icc a b)) (hae : (fun (t : ℝ) => ι (u t)) =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] w) {t : ℝ} (ht : t ∈ Set.Icc a b) : ‖w t‖ ^ 2 ≤ (⨍ (s : ℝ) in Set.Ioo a b, ‖ι (u s)‖ ^ 2) + 2 * ∫ (s : ℝ) in Set.Ioo a b, |(u' s) (u s)|

The C([a, b]; H) bound in a Gelfand triple. Let a < b, let u ∈ L²(a, b; V) be such that t ↦ ι.gelfandDual (ι (u t)) has weak derivative u' ∈ L²(a, b; V*) on (a, b), and let w be continuous on [a, b] and equal to ι ∘ u almost everywhere on (a, b). Then at every t ∈ [a, b], ‖w t‖² ≤ ⨍_{(a, b)} ‖ι u‖² + 2 ∫_{(a, b)} |u'(u)|.