Stability Bounded Pairing

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_integrable_mul_bounded_test {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {r : ENNReal} (hr : 1 ≤ r) {f φ : α → ℝ} (hf : MeasureTheory.MemLp f r μ) (hφ : MeasureTheory.MemLp φ ⊤ μ) : MeasureTheory.Integrable (fun (x : α) => f x * φ x) μ

On a finite-measure set, an Lᵖ field with p ≥ 1 has an integrable pairing with an essentially bounded scalar test.