lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top

English

If 0 < q and eLpNorm'_lt_top of f, then the Lintegral of ‖f‖^q is finite.

Русский

При 0<q и eLpNorm'_lt_top(f) имеют место, линтеграл от ||f||^q конечен.

LaTeX

$$$0< q\;\Rightarrow\; \int \! ||f||^q < \infty$ under the given hypothesis.$$

Lean4

theorem lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top {f : α → ε} (hq0_lt : 0 < q) (hfq : eLpNorm' f q μ < ∞) :
    ∫⁻ a, ‖f a‖ₑ ^ q ∂μ < ∞ := by
  rw [lintegral_rpow_enorm_eq_rpow_eLpNorm' hq0_lt]
  exact ENNReal.rpow_lt_top_of_nonneg (le_of_lt hq0_lt) (ne_of_lt hfq)

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