Stability Weighted Product Integrable

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_weighted_product_integrable {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {f g ψ : α → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) (hψ : MeasureTheory.MemLp ψ ⊤ μ) : MeasureTheory.Integrable (fun (x : α) => f x * g x * ψ x) μ

The product of two L² fields, weighted by a bounded scalar function, is integrable.