English
If ι is finite, the integral over the union of s_i across i∈ι equals the sum over i of integrals over s_i.
Русский
Если ι конечен, то интеграл по объединению s_i по i равен сумме интегралов по s_i.
LaTeX
$$$\\int_{\\bigcup_{i\\in ι} s_i} f = \\sum_{i\\in ι} \\int_{s_i} f$$$
Lean4
theorem integral_biUnion_finset {ι : Type*} (t : Finset ι) {s : ι → Set X} (hs : ∀ i ∈ t, MeasurableSet (s i))
(h's : Set.Pairwise (↑t) (Disjoint on s)) (hf : ∀ i ∈ t, IntegrableOn f (s i) μ) :
∫ x in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ x in s i, f x ∂μ := by
classical
induction t using Finset.induction_on with
| empty => simp
| insert _ _ hat
IH =>
simp only [Finset.coe_insert, Finset.forall_mem_insert, Set.pairwise_insert,
Finset.set_biUnion_insert] at hs hf h's ⊢
rw [setIntegral_union _ _ hf.1 (integrableOn_finset_iUnion.2 hf.2)]
· rw [Finset.sum_insert hat, IH hs.2 h's.1 hf.2]
· simp only [disjoint_iUnion_right]
exact fun i hi => (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1
· exact Finset.measurableSet_biUnion _ hs.2
