English
If f is a measurable map to a countable codomain β, then μ.map f equals the sum over b of μ(f^{-1}({b})) · dirac b.
Русский
Если f — измеримое отображение в счётное множество β, то μ.map f равна сумме по b из β μ(f^{-1}({b})) · δ_b.
LaTeX
$$$ μ.map f = \\sum b : β \\; μ (f^{-1}' { b }) \\cdot dirac b $$$
Lean4
/-- If `f` is a map with countable codomain, then `μ.map f` is a sum of Dirac measures. -/
theorem map_eq_sum [Countable β] [MeasurableSingletonClass β] (μ : Measure α) (f : α → β) (hf : Measurable f) :
μ.map f = sum fun b : β => μ (f ⁻¹' { b }) • dirac b :=
by
ext s
have : ∀ y ∈ s, MeasurableSet (f ⁻¹' { y }) := fun y _ => hf (measurableSet_singleton _)
simp [← tsum_measure_preimage_singleton (to_countable s) this, *, tsum_subtype s fun b => μ (f ⁻¹' { b }),
← indicator_mul_right s fun b => μ (f ⁻¹' { b })]
