English
Let f, g be α → E with measurable Lp and Lq norms finite, where p and q are conjugate. Then the integral of the product of their norms is bounded by the product of their p- and q-norms: ∫ ‖f‖ ‖g‖ ≤ (∫ ‖f‖^p)^{1/p} (∫ ‖g‖^q)^{1/q}.
Русский
Пусть f, g: α → E таковы, что их нормированные p-й и q-й моменты конечны при сопряжённых p, q. Тогда интеграл от произведения их норм оценивается как произведение соответствующих норм: ∫ ‖f‖^p ∂μ и ∫ ‖g‖^q ∂μ.
LaTeX
$$$\\displaystyle \\int_{\\alpha} \\|f(a)\\| \\cdot \\|g(a)\\| \\, d\\mu \\le \\left( \\int_{\\alpha} \\|f(a)\\|^{p} \\, d\\mu \\right)^{1/p} \\cdot \\left( \\int_{\\alpha} \\|g(a)\\|^{q} \\, d\\mu \\right)^{1/q}.$$$
Lean4
/-- Hölder's inequality for the integral of a product of norms. The integral of the product of two
norms of functions is bounded by the product of their `ℒp` and `ℒq` seminorms when `p` and `q` are
conjugate exponents. -/
theorem integral_mul_norm_le_Lp_mul_Lq {E} [NormedAddCommGroup E] {f g : α → E} {p q : ℝ} (hpq : p.HolderConjugate q)
(hf : MemLp f (ENNReal.ofReal p) μ) (hg : MemLp g (ENNReal.ofReal q) μ) :
∫ a, ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ a, ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ a, ‖g a‖ ^ q ∂μ) ^ (1 / q) := by
-- translate the Bochner integrals into Lebesgue integrals.
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
rotate_left
· exact Eventually.of_forall fun x => Real.rpow_nonneg (norm_nonneg _) _
· exact (hg.1.norm.aemeasurable.pow aemeasurable_const).aestronglyMeasurable
· exact Eventually.of_forall fun x => Real.rpow_nonneg (norm_nonneg _) _
· exact (hf.1.norm.aemeasurable.pow aemeasurable_const).aestronglyMeasurable
· exact Eventually.of_forall fun x => mul_nonneg (norm_nonneg _) (norm_nonneg _)
· exact hf.1.norm.mul hg.1.norm
rw [ENNReal.toReal_rpow, ENNReal.toReal_rpow, ← ENNReal.toReal_mul]
-- replace norms by nnnorm
have h_left : ∫⁻ a, ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ a, ((‖f ·‖ₑ) * (‖g ·‖ₑ)) a ∂μ := by
simp_rw [Pi.mul_apply, ← ofReal_norm_eq_enorm, ENNReal.ofReal_mul (norm_nonneg _)]
have h_right_f : ∫⁻ a, .ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ a, ‖f a‖ₑ ^ p ∂μ :=
by
refine lintegral_congr fun x => ?_
rw [← ofReal_norm_eq_enorm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.nonneg]
have h_right_g : ∫⁻ a, .ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ a, ‖g a‖ₑ ^ q ∂μ :=
by
refine lintegral_congr fun x => ?_
rw [← ofReal_norm_eq_enorm, ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hpq.symm.nonneg]
rw [h_left, h_right_f, h_right_g]
-- we can now apply `ENNReal.lintegral_mul_le_Lp_mul_Lq` (up to the `toReal` application)
refine ENNReal.toReal_mono ?_ ?_
· refine ENNReal.mul_ne_top ?_ ?_
· convert hf.eLpNorm_ne_top
rw [eLpNorm_eq_lintegral_rpow_enorm]
· rw [ENNReal.toReal_ofReal hpq.nonneg]
· rw [Ne, ENNReal.ofReal_eq_zero, not_le]
exact hpq.pos
· finiteness
· convert hg.eLpNorm_ne_top
rw [eLpNorm_eq_lintegral_rpow_enorm]
· rw [ENNReal.toReal_ofReal hpq.symm.nonneg]
· rw [Ne, ENNReal.ofReal_eq_zero, not_le]
exact hpq.symm.pos
· finiteness
·
exact
ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq hf.1.nnnorm.aemeasurable.coe_nnreal_ennreal
hg.1.nnnorm.aemeasurable.coe_nnreal_ennreal
