Stability Slice Energy Space Time

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_essSup_slice_energy_lt_top_spaceTime {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (ν : MeasureTheory.Measure β) [MeasureTheory.SFinite ν] (F : ℕ → α × β → E) (G : α × β → E) (hF : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) (μ.prod ν)) (hG : MeasureTheory.AEStronglyMeasurable G (μ.prod ν)) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 3 (μ.prod ν)) Filter.atTop (nhds 0)) (M : ENNReal) (hM : M < ⊤) (hbound : ∀ (n : ℕ), essSup (fun (t : β) => ∫⁻ (x : α), ‖F n (x, t)‖ₑ ^ 2 ∂μ) ν ≤ M) : essSup (fun (t : β) => ∫⁻ (x : α), ‖G (x, t)‖ₑ ^ 2 ∂μ) ν < ⊤

A uniform slice energy bound survives strong L³ convergence in the space-first product convention of def:sws (thm:stability).