English
For a countable family {s_i} with pairwise disjoint, the integral over the union equals the tsum of the integrals over each s_i.
Русский
Для счётной семейства {s_i} попарно дизъюнктных интеграл по объединению равен т-sum интегралов по каждому s_i.
LaTeX
$$$$ \int_{x \in \bigcup_i s_i} f(x) \; d\mu = \sum_{i} \int_{x \in s_i} f(x) \; d\mu $$$$
Lean4
theorem setIntegral_eq_zero_of_ae_eq_zero (ht_eq : ∀ᵐ x ∂μ, x ∈ t → f x = 0) : ∫ x in t, f x ∂μ = 0 :=
by
by_cases hf : AEStronglyMeasurable f (μ.restrict t); swap
· rw [integral_undef]
contrapose! hf
exact hf.1
have : ∫ x in t, hf.mk f x ∂μ = 0 := by
refine integral_eq_zero_of_ae ?_
rw [EventuallyEq, ae_restrict_iff (hf.stronglyMeasurable_mk.measurableSet_eq_fun stronglyMeasurable_zero)]
filter_upwards [ae_imp_of_ae_restrict hf.ae_eq_mk, ht_eq] with x hx h'x h''x
rw [← hx h''x]
exact h'x h''x
rw [← this]
exact integral_congr_ae hf.ae_eq_mk
