Stability Quadratic Product

Supporting estimates for the Navier–Stokes development.

theorem CKN.stabilityHolderThreeThreeThreeHalves : ENNReal.HolderTriple 3 3 (3 / 2)

theorem CKN.stability_tendsto_eLpNorm_product_three {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (F G : ℕ → α → ℝ) (f g : α → ℝ) (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 3 μ) (hG : ∀ (n : ℕ), MeasureTheory.MemLp (G n) 3 μ) (hf : MeasureTheory.MemLp f 3 μ) (hg : MeasureTheory.MemLp g 3 μ) (hFconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - f) 3 μ) Filter.atTop (nhds 0)) (hGconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (G n - g) 3 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => F n x * G n x - f x * g x) (3 / 2) μ) Filter.atTop (nhds 0)

Products of two strongly L³-convergent scalar fields converge strongly in L^{3/2}.