ennreal_tsum — Mathlib

English

If each f_i is a.e.-measurable, then tsum of f_i is a.e.-measurable.

Русский

Если каждая f_i а.е.-измерима, то tsum f_i — а.е.-измеримо.

LaTeX

$$$\forall i, \text{AEMeasurable}(f_i) \Rightarrow \text{AEMeasurable}(\sum_i f_i)$$$

Lean4

@[measurability, fun_prop]
theorem ennreal_tsum {ι} [Countable ι] {f : ι → α → ℝ≥0∞} {μ : Measure α} (h : ∀ i, AEMeasurable (f i) μ) :
    AEMeasurable (fun x => ∑' i, f i x) μ :=
  by
  simp_rw [ENNReal.tsum_eq_iSup_sum]
  exact .iSup fun s ↦ Finset.aemeasurable_fun_sum s fun i _ => h i

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