Stability Slice Energy #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.stability_essSup_slice_energy_lt_top
{α : Type u_1}
{β : Type u_2}
{E : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[NormedAddCommGroup E]
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(ν : MeasureTheory.Measure β)
(F : ℕ → β × α → E)
(G : β × α → E)
(hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 3 (ν.prod μ)) Filter.atTop (nhds 0))
(hF : ∀ (n : ℕ), ∀ᵐ (t : β) ∂ν, AEMeasurable (fun (x : α) => ‖F n (t, x)‖ₑ ^ 2) μ)
(M : ENNReal)
(hM : M < ⊤)
(hbound : ∀ (n : ℕ), essSup (fun (t : β) => ∫⁻ (x : α), ‖F n (t, x)‖ₑ ^ 2 ∂μ) ν ≤ M)
:
The essential-supremum slice energy bound persists under strong space-time
convergence (thm:stability).