Continuity of weighted kinetic energies

In the proof of lem:forced-tails the localized energy inequality is passed to the endpoints of a time interval using the continuity of t ↦ ∫ |u(x,t)|² q(x) dx for a bounded weight q. For a velocity whose slices form a continuous curve in L² (as in lem:regularised-forced) this follows from |∫ (|a|² - |b|²) q| ≤ ‖a - b‖₂ ‖q (a + b)‖₂.

theorem CKN.Leray.forcedTails_weightedEnergy_continuousOn (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hSlice : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hcont : Continuous fun (t : ↑(Set.Ici 0)) => realVectorL2OfCoordinateFunction (fun (x : Foundation.Parabolic.Vec3) => u (x, ↑t)) ⋯) {q : Foundation.Parabolic.Vec3 → ℝ} (hq : Measurable q) {C : ℝ} (hqC : ∀ (x : Foundation.Parabolic.Vec3), |q x| ≤ C) : ContinuousOn (fun (τ : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), Foundation.Parabolic.vec3EuclideanNorm (u (x, τ)) ^ 2 * q x) (Set.Ici 0)

The weighted kinetic energy t ↦ ∫ |u(x,t)|² q(x) dx of a velocity whose slices form a continuous curve in L² is continuous on [0,∞) for every bounded measurable weight q (lem:forced-tails).