lintegral_lt_top — Mathlib

English

Let f be a simple function with finite μ-measurable support and finite values almost everywhere; then f.lintegral μ < ∞.

Русский

Пусть f — простая функция с конечной μ-опорой и конечными значениями почти повсеместно; тогда f.lintegral μ < ∞.

LaTeX

$$$f \in \mathsf{SimpleFunc}$, $\mathrm{FinMeasSupp}(f,\mu)$ и $\forall^{\!a\!\partial\mu} f(a) \neq \infty \Rightarrow f.\mathrm{lintegral}\,\mu < \infty$$$

Lean4

theorem lintegral_lt_top {f : α →ₛ ℝ≥0∞} (hm : f.FinMeasSupp μ) (hf : ∀ᵐ a ∂μ, f a ≠ ∞) : f.lintegral μ < ∞ :=
  by
  refine sum_lt_top.2 fun a ha => ?_
  rcases eq_or_ne a ∞ with (rfl | ha)
  · simp only [ae_iff, Ne, Classical.not_not] at hf
    simp [Set.preimage, hf]
  · by_cases ha0 : a = 0
    · subst a
      simp
    · exact mul_lt_top ha.lt_top (finMeasSupp_iff.1 hm _ ha0)

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