English
For any q > 0, the Lp-norm with exponent q is dominated by the EssSup-based bound.
Русский
Для любого q > 0 норма Lp ограничена сверху по эскизной границе, задаваемой EssSup.
LaTeX
$$$0 < q \\Rightarrow eLpNorm' f q μ \\le eLpNormEssSup f μ \\cdot μ(\\mathrm{univ})^{1/q}$$$
Lean4
theorem eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ {q : ℝ} (hq_pos : 0 < q) :
eLpNorm' f q μ ≤ eLpNormEssSup f μ * μ Set.univ ^ (1 / q) :=
by
have h_le : (∫⁻ a : α, ‖f a‖ₑ ^ q ∂μ) ≤ ∫⁻ _ : α, eLpNormEssSup f μ ^ q ∂μ :=
by
refine lintegral_mono_ae ?_
have h_nnnorm_le_eLpNorm_ess_sup := enorm_ae_le_eLpNormEssSup f μ
exact h_nnnorm_le_eLpNorm_ess_sup.mono fun x hx => by gcongr
rw [eLpNorm', ← ENNReal.rpow_one (eLpNormEssSup f μ)]
nth_rw 2 [← mul_inv_cancel₀ (ne_of_lt hq_pos).symm]
rw [ENNReal.rpow_mul, one_div, ← ENNReal.mul_rpow_of_nonneg _ _ (by simp [hq_pos.le] : 0 ≤ q⁻¹)]
gcongr
rwa [lintegral_const] at h_le