English
For a measurable set s in β, the measure of s under p.bindOnSupport f equals the weighted sum ∑' a p(a) times the measure of s under f(a, ha).
Русский
Для измеримой множества s в β мера равна взвешенной сумме ∑' a p(a) умноженной на меру s у f(a, ha).
LaTeX
$$$$ (p.bindOnSupport f).toMeasure s = \\sum' a, p(a) \\cdot (f(a, h)).toMeasure(s) $$$$
Lean4
/-- The measure of a set under `p.bind f` is the sum over `a : α`
of the probability of `a` under `p` times the measure of the set under `f a`. -/
@[simp]
theorem toMeasure_bind_apply [MeasurableSpace β] (hs : MeasurableSet s) :
(p.bind f).toMeasure s = ∑' a, p a * (f a).toMeasure s :=
(toMeasure_apply_eq_toOuterMeasure_apply (p.bind f) hs).trans
((toOuterMeasure_bind_apply p f s).trans
(tsum_congr fun a => congr_arg (fun x => p a * x) (toMeasure_apply_eq_toOuterMeasure_apply (f a) hs).symm))
