One-dimensional time calculus for the localized vorticity energy

A function of time with an integrable weak derivative on (a, τ), and with a continuous version taking the value c₀ at a, is almost everywhere the primitive c₀ + ∫ₐᵗ G. The square of such a primitive satisfies the energy identity (c₀ + ∫ₐᵗ G)² = c₀² + ∫ₐᵗ 2 (c₀ + ∫ₐˢ G) G(s) ds. These are the time steps of the energy argument in lem:localized-vorticity-energy of the Escauriaza–Seregin–Šverák manuscript.

theorem CKN.vlTime_sq_primitive {a t c : ℝ} {G : ℝ → ℝ} (hG : IntervalIntegrable G MeasureTheory.volume a t) : (c + ∫ (s : ℝ) in a..t, G s) ^ 2 = c ^ 2 + ∫ (s : ℝ) in a..t, 2 * (c + ∫ (r : ℝ) in a..s, G r) * G s

The energy identity for the square of an absolutely continuous primitive.

theorem CKN.vlTime_eq_primitive_of_trace {a τ : ℝ} (hat : a < τ) {f G c : ℝ → ℝ} {c₀ : ℝ} (hf : MeasureTheory.IntegrableOn f (Set.Ioo a τ) MeasureTheory.volume) (hG : MeasureTheory.IntegrableOn G (Set.Ioo a τ) MeasureTheory.volume) (hweak : HasWeakDerivOn (Set.Ioo a τ) f G) (hc : ContinuousOn c (Set.Icc a τ)) (hca : c a = c₀) (hcf : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a τ), c t = f t) : (∀ t ∈ Set.Icc a τ, c t = c₀ + ∫ (s : ℝ) in a..t, G s) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a τ), f t = c₀ + ∫ (s : ℝ) in a..t, G s

A weak time derivative together with a continuous version with value c₀ at the initial time determines the function as the primitive from c₀.