integrable_enorm_rpow_iff — Mathlib

English

For AEStronglyMeasurable f, p ≠ 0, p ≠ ∞, Integrable ‖f‖^p ≡ MemLp f p μ.

Русский

Для AEStronglyMeasurable f и p ≠ 0, ∞, Integrable ‖f‖^p эквивалентно MemLp f p μ.

LaTeX

$$AEStronglyMeasurable f μ ∧ p ≠ 0 ∧ p ≠ ∞ ⇒ (Integrable (‖f‖^p.toReal) μ ↔ MemLp f p μ)$$

Lean4

theorem integrable_enorm_rpow_iff {f : α → ε} {p : ℝ≥0∞} (hf : AEStronglyMeasurable f μ) (p_zero : p ≠ 0)
    (p_top : p ≠ ∞) : Integrable (fun x : α => ‖f x‖ₑ ^ p.toReal) μ ↔ MemLp f p μ := by
  rw [← memLp_enorm_rpow_iff (q := p) hf p_zero p_top, ← memLp_one_iff_integrable, ENNReal.div_self p_zero p_top]

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