Holder Triple Products

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Measure.eLpNorm_mul_le_two_three {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.eLpNorm (fun (x : α) => f x * g x) (ENNReal.ofReal (6 / 5)) μ ≤ MeasureTheory.eLpNorm f (ENNReal.ofReal 2) μ * MeasureTheory.eLpNorm g (ENNReal.ofReal 3) μ

Hölder's inequality for the exponent triple (2, 3; 6/5): for f ∈ L² and g ∈ L³, the product f·g is in L^{6/5} with the corresponding norm bound.

theorem CKN.Foundation.Measure.eLpNorm_mul_le_three_three {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : MeasureTheory.eLpNorm (fun (x : α) => f x * g x) (ENNReal.ofReal (3 / 2)) μ ≤ MeasureTheory.eLpNorm f (ENNReal.ofReal 3) μ * MeasureTheory.eLpNorm g (ENNReal.ofReal 3) μ

Hölder's inequality for the exponent triple (3, 3; 3/2): for f, g ∈ L³, the product f·g is in L^{3/2} with the corresponding norm bound.

theorem CKN.Foundation.Measure.eLpNorm_mul_le_ofReal_mul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {a f : α → ℝ} {C : ℝ} (ha : MeasureTheory.AEStronglyMeasurable a μ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hC : 0 ≤ C) (haC : ∀ᵐ (x : α) ∂μ, |a x| ≤ C) {p : ENNReal} : MeasureTheory.eLpNorm (fun (x : α) => a x * f x) p μ ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm f p μ

Multiplying an Lᵖ function by an a.e.-bounded function a with |a| ≤ C a.e. preserves the Lᵖ norm up to a factor of C.