English
Let s_i be null-measurable and pairwise aedisjoint. If f is integrable on the union, then the sum of integrals over the s_i converges to the integral over the union (ae-disjoint version).
Русский
Пусть множества s_i слабо измеримы и попарно ae-независимы. Если f интегрируем на объединении, то сумма интегралов по s_i сходится к интегралу по объединению (ae-непересечение).
LaTeX
$$$$ \text{HasSum}\Big( n \mapsto \int_{x \in s_n} f(x) \, d\mu \Big) \;\Big( \int_{x \in \bigcup_{n} s_n} f(x) \, d\mu \Big) $$$$
Lean4
theorem hasSum_integral_iUnion_ae {ι : Type*} [Countable ι] {s : ι → Set X} (hm : ∀ i, NullMeasurableSet (s i) μ)
(hd : Pairwise (AEDisjoint μ on s)) (hfi : IntegrableOn f (⋃ i, s i) μ) :
HasSum (fun n => ∫ x in s n, f x ∂μ) (∫ x in ⋃ n, s n, f x ∂μ) :=
by
simp only [IntegrableOn, Measure.restrict_iUnion_ae hd hm] at hfi ⊢
exact hasSum_integral_measure hfi
