eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ

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

Похожие утверждения