English
If X takes finitely many values and is measurable, then μ = sum over x of μ(X^{-1}{x}) • μ[|X ← x].
Русский
Если X принимает конечное число значений и измерим, то мера μ является суммой по фиберам: μ = ∑_x μ(X^{-1}{x}) • μ[|X ← x].
LaTeX
$$$\\sum_{x} μ(X^{-1}\\{x\\}) \\cdot μ[|X \\leftarrow x] = μ$$$
Lean4
/-- The **law of total probability** for a random variable taking finitely many values: a measure
`μ` can be expressed as a linear combination of its conditional measures `μ[|X ← x]` on fibers of a
random variable `X` valued in a fintype. -/
theorem sum_meas_smul_cond_fiber {X : Ω → α} (hX : Measurable X) (μ : Measure Ω) [IsFiniteMeasure μ] :
∑ x, μ (X ⁻¹' { x }) • μ[|X ← x] = μ := by
ext E hE
calc
_ = ∑ x, μ (X ⁻¹' { x } ∩ E) :=
by
simp only [Measure.coe_finset_sum, Measure.coe_smul, Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
simp_rw [mul_comm (μ _), cond_mul_eq_inter (hX (.singleton _))]
_ = _ := by
have : ⋃ x ∈ Finset.univ, X ⁻¹' { x } ∩ E = E := by ext; simp
rw [← measure_biUnion_finset _ fun _ _ ↦ (hX (.singleton _)).inter hE, this]
aesop (add simp [PairwiseDisjoint, Set.Pairwise, Function.onFun, disjoint_left])
