TODO

Less explicit arguments to cond_eq_zero_of_meas_eq_zero

theorem ProbabilityTheory.sum_meas_smul_cond_fiber' {Ω : Type u_1} {α : Type u_2} {m : MeasurableSpace Ω} [MeasurableSpace α] [MeasurableSingletonClass α] {X : Ω → α} (hX : Measurable X) [finX : FiniteRange X] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ((FiniteRange.toFinset X).sum fun (x : α) => μ (X ⁻¹' {x}) • ProbabilityTheory.cond μ (X ⁻¹' {x})) = μ

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.