Reg Tails Time Energy

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.regTails_timeGradientNorm_sq_integral_bound {α : Type} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {B : ℝ} (F : α × ℝ → ℝ) (hFmeas : Measurable F) (hTotal : 2 * ∫⁻ (z : α × ℝ), ENNReal.ofReal (F z) ∂μ.prod (MeasureTheory.volume.restrict (Set.Ioi 0)) ≤ ENNReal.ofReal (B ^ 2)) (T : ℝ) : 0 < T → have g := fun (t : ℝ) => √(∫⁻ (x : α), ENNReal.ofReal (F (x, t)) ∂μ).toReal; MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ioo 0 T)) ∧ ∫ (t : ℝ) in Set.Ioo 0 T, g t ^ 2 ≤ B ^ 2 / 2 ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫⁻ (x : α), ENNReal.ofReal (F (x, t)) ∂μ ≠ ⊤

The spatial gradient size is square integrable in time when its nonnegative spacetime density has finite integral.