English
The sum over x of s.indicator(μ({x})) equals μ(s) for measurable s in a countable space.
Русский
Сумма по x индикатору s.indicator(μ({x})) даёт μ(s) для измеримого s на счётном пространстве.
LaTeX
$$$ ∑' x : α,\; s.indicator (fun x => μ { x }) x = μ s $$$
Lean4
/-- Given that `α` is a countable, measurable space with all singleton sets measurable,
write the measure of a set `s` as the sum of the measure of `{x}` for all `x ∈ s`. -/
theorem tsum_indicator_apply_singleton [Countable α] [MeasurableSingletonClass α] (μ : Measure α) (s : Set α)
(hs : MeasurableSet s) : (∑' x : α, s.indicator (fun x => μ { x }) x) = μ s := by
classical
calc
(∑' x : α, s.indicator (fun x => μ { x }) x) = Measure.sum (fun a => μ { a } • Measure.dirac a) s := by
simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply, Set.indicator_apply,
mul_ite, Pi.one_apply, mul_one, mul_zero]
_ = μ s := by rw [μ.sum_smul_dirac]
