English
For any q > 0, the Lp-norm with exponent q is bounded by the EssSup norm of f times μ(univ)^(1/q).
Русский
Для любого q > 0 норма Lp с показателем q ограничена по норме EssSup функции f, умноженной на μ(всё пространство)^(1/q).
LaTeX
$$$q \\in \\mathbb{R},\\ q > 0 \\Rightarrow eLpNorm' f q μ \\le eLpNormEssSup f μ \\cdot μ(\\mathrm{univ})^{1/q}$$$
Lean4
theorem eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ {p q : ℝ} (hp0_lt : 0 < p) (hpq : p ≤ q)
(hf : AEStronglyMeasurable f μ) : eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q) :=
by
have hq0_lt : 0 < q := lt_of_lt_of_le hp0_lt hpq
by_cases hpq_eq : p = q
· rw [hpq_eq, sub_self, ENNReal.rpow_zero, mul_one]
have hpq : p < q := lt_of_le_of_ne hpq hpq_eq
let g := fun _ : α => (1 : ℝ≥0∞)
have h_rw : (∫⁻ a, ‖f a‖ₑ ^ p ∂μ) = ∫⁻ a, (‖f a‖ₑ * g a) ^ p ∂μ := lintegral_congr fun a => by simp [g]
repeat' rw [eLpNorm'_eq_lintegral_enorm]
rw [h_rw]
let r := p * q / (q - p)
have hpqr : 1 / p = 1 / q + 1 / r := by simp [field]
calc
(∫⁻ a : α, (‖f a‖ₑ * g a) ^ p ∂μ) ^ (1 / p) ≤
(∫⁻ a : α, ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * (∫⁻ a : α, g a ^ r ∂μ) ^ (1 / r) :=
ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hp0_lt hpq hpqr μ hf.enorm aemeasurable_const
_ = (∫⁻ a : α, ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) * μ Set.univ ^ (1 / p - 1 / q) := by rw [hpqr]; simp [r, g]
