ennreal_tsum — Mathlib

English

If each f_i is measurable, then the tsum over i of f_i is measurable.

Русский

Если каждое f_i измеримо, то сумма tsum по i измерима.

LaTeX

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

Lean4

/-- note: `ℝ≥0∞` can probably be generalized in a future version of this lemma. -/
@[measurability, fun_prop]
theorem ennreal_tsum {ι} [Countable ι] {f : ι → α → ℝ≥0∞} (h : ∀ i, Measurable (f i)) :
    Measurable fun x => ∑' i, f i x := by
  simp_rw [ENNReal.tsum_eq_iSup_sum]
  exact .iSup fun s ↦ s.measurable_fun_sum fun i _ => h i

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