English
If α is countable and f is integrable on a subset s, then ∫ a in s f(a) dμ equals the sum over a in s of μ.real{a} f(a).
Русский
Если α счётно, и f интегрируема на s, то интеграл по s равен сумме по a∈s μ.real{a} f(a).
LaTeX
$$$\\displaystyle \\int_{a \\in s} f(a) \\, d\\mu = \\sum_{a \\in s} \\mu_{\\mathbb{R}}(\\{a\\}) \\cdot f(a)$$$
Lean4
theorem integral_countable [MeasurableSingletonClass α] (f : α → E) {s : Set α} (hs : s.Countable)
(hf : IntegrableOn f s μ) : ∫ a in s, f a ∂μ = ∑' a : s, μ.real {(a : α)} • f a :=
by
have hi : Countable { x // x ∈ s } := Iff.mpr countable_coe_iff hs
have hf' : Integrable (fun (x : s) => f x) (Measure.comap Subtype.val μ) :=
by
rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf
· apply hf
· exact Integrable.aestronglyMeasurable hf
· exact Measurable.aemeasurable measurable_subtype_coe
· exact Countable.measurableSet hs
rw [← integral_subtype_comap hs.measurableSet, integral_countable' hf']
congr 1 with a : 1
rw [measureReal_def,
Measure.comap_apply Subtype.val Subtype.coe_injective
(fun s' hs' => MeasurableSet.subtype_image (Countable.measurableSet hs) hs') _ (MeasurableSet.singleton a)]
simp [measureReal_def]
