English
For a finite measure μ, the real-valued integral of 1 over a set s equals μ s, i.e., ∫_s 1 dμ = μ s, and its ENNReal version matches the measure via ofReal.
Русский
Для конечной меры μ интеграл по множеству s от константы 1 равен μ(s) и согласуется с ENNReal через ofReal.
LaTeX
$$$$\operatorname{ofReal}\left(\int_{x \in s} 1 \; dμ\right) = μ(s).$$$$
Lean4
/-- **Inclusion-exclusion principle** for the integral of a function over a union.
The integral of a function `f` over the union of the `s i` over `i ∈ t` is the alternating sum of
the integrals of `f` over the intersections of the `s i`. -/
theorem integral_biUnion_eq_sum_powerset {ι : Type*} {t : Finset ι} {s : ι → Set X} (hs : ∀ i ∈ t, MeasurableSet (s i))
(hf : ∀ i ∈ t, IntegrableOn f (s i) μ) :
∫ x in ⋃ i ∈ t, s i, f x ∂μ = ∑ u ∈ t.powerset with u.Nonempty, (-1 : ℝ) ^ (#u + 1) • ∫ x in ⋂ i ∈ u, s i, f x ∂μ :=
by
simp_rw [← integral_smul, ← integral_indicator (Finset.measurableSet_biUnion _ hs)]
have A (u) (hu : u ∈ t.powerset.filter (·.Nonempty)) : MeasurableSet (⋂ i ∈ u, s i) :=
by
refine u.measurableSet_biInter fun i hi ↦ hs i ?_
aesop
have :
∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1 : ℝ) ^ (#x + 1) • f a ∂μ =
∑ x ∈ t.powerset with x.Nonempty, ∫ a, indicator (⋂ i ∈ x, s i) (fun a ↦ (-1 : ℝ) ^ (#x + 1) • f a) a ∂μ :=
by
apply Finset.sum_congr rfl (fun x hx ↦ ?_)
rw [← integral_indicator (A x hx)]
rw [this, ← integral_finset_sum]; swap
· intro u hu
rw [integrable_indicator_iff (A u hu)]
apply Integrable.smul
simp only [Finset.mem_filter, Finset.mem_powerset] at hu
rcases hu.2 with ⟨i, hi⟩
exact (hf i (hu.1 hi)).mono (biInter_subset_of_mem hi) le_rfl
congr with x
convert Finset.indicator_biUnion_eq_sum_powerset t s f x with u hu
rw [indicator_smul_apply]
norm_cast
