English
For any f and measurable s, the measure of s under p.bindOnSupport f equals the sum ∑' a p(a) times the measure of s under (f a h).
Русский
Для любой f и измеримого s мера s в p.bindOnSupport f равна сумме ∑' a p(a) ⋅ (f(a,h)).toMeasure(s).
LaTeX
$$$$ (\\mathrm{bindOnSupport} f).\\mathrm{toMeasure} (s) = \\sum' a \\, p(a) \\cdot (f(a,h)).\\mathrm{toMeasure}(s) $$$$
Lean4
/-- The measure of a set under `p.bindOnSupport f` is the sum over `a : α`
of the probability of `a` under `p` times the measure of the set under `f a _`.
The additional if statement is needed since `f` is only a partial function. -/
@[simp]
theorem toMeasure_bindOnSupport_apply [MeasurableSpace β] (hs : MeasurableSet s) :
(p.bindOnSupport f).toMeasure s = ∑' a, p a * if h : p a = 0 then 0 else (f a h).toMeasure s := by
simp only [toMeasure_apply_eq_toOuterMeasure_apply _ hs, toOuterMeasure_bindOnSupport_apply]
