integral_iUnion_ae — Mathlib

English

If null-measurability and aedisjoint conditions hold for a family {s_i}, then HasSum holds for the integrals over s_i equalling the integral over their union.

Русский

Если выполняются условия нулевой измеримости и ae-диссипации для семейства {s_i}, то имеет место HasSum для интегралов над s_i, равный интегралу по их объединению.

LaTeX

$$$$ \text{HasSum}\left( n \mapsto \int_{x \in s_n} f(x) \, d\mu \right) = \int_{x \in \bigcup_n s_n} f(x) \, d\mu $$$$

Lean4

theorem integral_iUnion_ae {ι : Type*} [Countable ι] {s : ι → Set X} (hm : ∀ i, NullMeasurableSet (s i) μ)
    (hd : Pairwise (AEDisjoint μ on s)) (hfi : IntegrableOn f (⋃ i, s i) μ) :
    ∫ x in ⋃ n, s n, f x ∂μ = ∑' n, ∫ x in s n, f x ∂μ :=
  (HasSum.tsum_eq (hasSum_integral_iUnion_ae hm hd hfi)).symm

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