Weak product rules for symmetric bilinear forms

Let B : V →L[ℝ] V →L[ℝ] ℝ be a continuous symmetric bilinear form on a real Banach space V, and let u : E → V be square integrable on an open set Ω of a finite-dimensional space E. Suppose that the V*-valued function x ↦ B (u x) has a weak derivative u' in a direction v, square integrable on Ω. This file proves the product rule

∂_v B(u, u) = 2 u'(u) weakly on Ω

(TauCeti.HasWeakLineDerivOn.bilin_self). Neither u itself nor x ↦ B(u x, u x) is assumed to be differentiable in any sense: only the image of u in V* has a derivative, and it is paired back with u.

Polarization gives the mixed rule ∂_v B(u, w) = u'(w) + w'(u) (TauCeti.HasWeakLineDerivOn.bilin).

The case of interest is a Gelfand triple V ↪ H ↪ V* given by ι : V →L[ℝ] H, with B(x, y) = ⟪ι x, ι y⟫. Then the rule reads ∂_v ‖ι u‖² = 2 u'(u) (TauCeti.HasWeakLineDerivOn.norm_sq_of_gelfandDual). For E = ℝ and v = 1 this is the identity d/dt ‖u(t)‖²_H = 2 ⟨u'(t), u(t)⟩ for u ∈ L²(0, T; V) with u' ∈ L²(0, T; V*), the energy identity behind existence and uniqueness for linear parabolic equations.

Main declarations

• TauCeti.HasWeakLineDerivOn.bilin: the mixed product rule for two functions.
• TauCeti.HasWeakLineDerivOn.bilin_self: the weak product rule ∂_v B(u, u) = 2 u'(u).
• TauCeti.HasWeakLineDerivOn.norm_sq_of_gelfandDual: its Gelfand-triple form ∂_v ‖ι u‖² = 2 u'(u).

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.bilin_self {E : Type u_1} {V : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {Ω : TopologicalSpace.Opens E} {v : E} {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : B.flip = B) {u : E → V} {u' : E → StrongDual ℝ V} (h : HasWeakLineDerivOn μ Ω (fun (x : E) => B (u x)) u' v) (hu : MeasureTheory.MemLp u 2 (μ.restrict ↑Ω)) (hu' : MeasureTheory.MemLp u' 2 (μ.restrict ↑Ω)) : HasWeakLineDerivOn μ Ω (fun (x : E) => (B (u x)) (u x)) (fun (x : E) => 2 * (u' x) (u x)) v

The weak product rule for a quadratic form. Let B be a continuous symmetric bilinear form on V, and let u ∈ L²(Ω; V). If the V*-valued function x ↦ B (u x) has weak derivative u' ∈ L²(Ω; V*) in the direction v on Ω, then x ↦ B (u x) (u x) has weak derivative x ↦ 2 u'(x)(u x) in the direction v on Ω.

theorem TauCeti.HasWeakLineDerivOn.bilin {E : Type u_1} {V : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {Ω : TopologicalSpace.Opens E} {v : E} {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : B.flip = B) {u w : E → V} {u' w' : E → StrongDual ℝ V} (h : HasWeakLineDerivOn μ Ω (fun (x : E) => B (u x)) u' v) (hw : HasWeakLineDerivOn μ Ω (fun (x : E) => B (w x)) w' v) (hu : MeasureTheory.MemLp u 2 (μ.restrict ↑Ω)) (hu' : MeasureTheory.MemLp u' 2 (μ.restrict ↑Ω)) (hwL : MeasureTheory.MemLp w 2 (μ.restrict ↑Ω)) (hw' : MeasureTheory.MemLp w' 2 (μ.restrict ↑Ω)) : HasWeakLineDerivOn μ Ω (fun (x : E) => (B (u x)) (w x)) (fun (x : E) => (u' x) (w x) + (w' x) (u x)) v

The mixed weak product rule for a symmetric bilinear form. For square-integrable u and w, if B u and B w have square-integrable weak derivatives u' and w', then B(u, w) has weak derivative u'(w) + w'(u). Only the dual-valued images need to be weakly differentiable.

theorem TauCeti.HasWeakLineDerivOn.norm_sq_of_gelfandDual {E : Type u_1} {V : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {Ω : TopologicalSpace.Opens E} {v : E} {H : Type u_3} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : V →L[ℝ] H} {u : E → V} {u' : E → StrongDual ℝ V} (h : HasWeakLineDerivOn μ Ω (fun (x : E) => ι.gelfandDual (ι (u x))) u' v) (hu : MeasureTheory.MemLp u 2 (μ.restrict ↑Ω)) (hu' : MeasureTheory.MemLp u' 2 (μ.restrict ↑Ω)) : HasWeakLineDerivOn μ Ω (fun (x : E) => ‖ι (u x)‖ ^ 2) (fun (x : E) => 2 * (u' x) (u x)) v

The weak derivative of ‖ι u‖² in a Gelfand triple. Let ι : V →L[ℝ] H and u ∈ L²(Ω; V). If the V*-valued function x ↦ ι.gelfandDual (ι (u x)), that is u viewed in V* through V → H → V*, has weak derivative u' ∈ L²(Ω; V*) in the direction v on Ω, then x ↦ ‖ι (u x)‖² has weak derivative x ↦ 2 u'(x)(u x) in the direction v on Ω.