hasFiniteIntegral_count_iff_enorm

English

For a function f: α → ε that is summable, the finite integral condition holds equivalently.

Русский

Для функции f: α → ε, которую можно суммировать, условие конечного интеграла эквивалентно.

LaTeX

$$Summable (‖f‖) ⇔ HasFiniteIntegral f μ (under counting or relevant measure)$$

Lean4

/-- A function has finite integral for the counting measure iff its enorm has finite `tsum`. -/
-- Note that asking for mere summability makes no sense, as every sequence in ℝ≥0∞ is summable.

theorem hasFiniteIntegral_count_iff_enorm {f : α → ε} : HasFiniteIntegral f Measure.count ↔ tsum (‖f ·‖ₑ) < ⊤ := by
  simp only [hasFiniteIntegral_iff_enorm, lintegral_count]

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