The law of total probability over countably many fibres #
A finite measure is the sum, over the values of a random variable with countably many values, of its conditional measures on the fibres weighted by the masses of the fibres:
μ = Measure.sum fun b => μ (f ⁻¹' {b}) • μ[|f ⁻¹' {b}].
Mathlib's ProbabilityTheory.sum_meas_smul_cond_fiber is the same decomposition for a random
variable valued in a Fintype; this file extends it to countable value spaces with measurable
singletons, where the finite sum of measures becomes MeasureTheory.Measure.sum. Fibres of mass
zero contribute nothing, so no positivity hypothesis on the fibres is needed.
Main results #
theorem
ProbabilityTheory.sum_meas_smul_cond_fiber_of_countable
{Ω : Type u_1}
{β : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace β]
[Countable β]
[MeasurableSingletonClass β]
{f : Ω → β}
(hf : Measurable f)
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
:
The law of total probability for a random variable with countably many values: a finite
measure μ is the sum of its conditional measures on the fibres of a measurable f, each weighted
by the mass of its fibre.