eLpNorm_lt_top_of_finite — Mathlib

English

If α is finite and μ is a finite measure, then eLpNorm f p μ is finite for any p ∈ [0, ∞].

Русский

Если α конечна и μ — конечная мера, тогда eLpNorm f p μ конечна для любых p ∈ [0, ∞].

LaTeX

$$eLpNorm f p μ < ∞$$

Lean4

theorem eLpNorm_lt_top_of_finite [Finite α] [IsFiniteMeasure μ] : eLpNorm f p μ < ∞ :=
  by
  obtain rfl | hp₀ := eq_or_ne p 0
  · simp
  obtain rfl | hp := eq_or_ne p ∞
  · simp only [eLpNorm_exponent_top, eLpNormEssSup_lt_top_iff_isBoundedUnder]
    exact .le_of_finite
  rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp]
  refine IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal μ ?_
  simp_rw [enorm, ← ENNReal.coe_rpow_of_nonneg _ ENNReal.toReal_nonneg]
  norm_cast
  exact Finite.exists_le _

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