English
For any q, eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ: the Lp'-norm is controlled by the EssSup norm times a power of μ(univ).
Русский
Неравенство, связывающее eLpNorm' с eLpNormEssSup через μ(univ).
LaTeX
$$$eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ \\text{ with appropriate exponents and HolderTriple}$$$
Lean4
theorem eLpNorm'_le_eLpNorm'_mul_eLpNorm' {p q r : ℝ} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
(b : E → F → G) (c : ℝ≥0) (h : ∀ᵐ x ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) (hro_lt : 0 < r) (hrp : r < p)
(hpqr : 1 / r = 1 / p + 1 / q) : eLpNorm' (fun x => b (f x) (g x)) r μ ≤ c * eLpNorm' f p μ * eLpNorm' g q μ := by
calc
eLpNorm' (fun x => b (f x) (g x)) r μ ≤ eLpNorm' (fun x ↦ (c : ℝ) • ‖f x‖ * ‖g x‖) r μ :=
by
simp only [eLpNorm']
refine
(ENNReal.rpow_le_rpow_iff <| one_div_pos.mpr hro_lt).mpr <|
lintegral_mono_ae <| h.mono fun a ha ↦ (ENNReal.rpow_le_rpow_iff hro_lt).mpr <| ?_
simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe, ← NNReal.coe_le_coe]
simpa [Real.nnnorm_of_nonneg (by positivity)] using ha
_ ≤ c * eLpNorm' f p μ * eLpNorm' g q μ :=
by
simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm'_const_smul _ hro_lt]
rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
gcongr
simpa only [eLpNorm', enorm_mul, enorm_norm] using
ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hro_lt hrp hpqr μ hf.enorm hg.enorm
