nnreal_tsum — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[measurability, fun_prop]
theorem nnreal_tsum {α : Type*} {_ : MeasurableSpace α} {ι : Type*} [Countable ι] {f : ι → α → NNReal} {μ : Measure α}
    (h : ∀ i : ι, AEMeasurable (f i) μ) : AEMeasurable (fun x : α => ∑' i : ι, f i x) μ :=
  by
  simp_rw [NNReal.tsum_eq_toNNReal_tsum]
  exact (AEMeasurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal

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