The energy of the mollified velocity at a point

At every spatial point the mollified forced regularized velocity is an absolutely continuous function of time on bounded intervals, with derivative minus the source. Against a smooth time profile vanishing near the ends of an interval, the square of the mollified velocity therefore satisfies ∫ w² ∂ₜψ = 2 ∫ w S ψ. This is the time part of the local energy inequality eq:reg-local-energy-forced.

theorem CKN.Leray.deriv_eq_zero_of_eventually_eq_zero {g : ℝ → ℝ} {t : ℝ} (h : g =ᶠ[nhds t] fun (x : ℝ) => 0) : deriv g t = 0

theorem CKN.Leray.integral_leW_sq_time (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsInJ a) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hf : IsLocallySquareIntegrableForce f) {η : Foundation.Parabolic.Vec3 → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (x : Foundation.Parabolic.Vec3) (k : Fin 3) {T : ℝ} (hT : 0 < T) {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {c d : ℝ} (hc : 0 < c) (hcd : c < d) (hdT : d < T) (hψs : ∀ t ∉ Set.Ioo c d, ψ t = 0) (hSi : MeasureTheory.IntegrableOn (fun (t : ℝ) => leSF ρ ε hε ha hf η x t k) (Set.Ioo 0 T) MeasureTheory.volume) : ∫ (t : ℝ) in Set.Ioo 0 T, leW ρ ε hε ha hf η x t k ^ 2 * deriv ψ t = 2 * ∫ (t : ℝ) in Set.Ioo 0 T, leW ρ ε hε ha hf η x t k * leSF ρ ε hε ha hf η x t k * ψ t

The time energy identity of the mollified velocity at a point.