English
Binding in two steps is associative: bind(bind(m, f), g) = bind(m, a ↦ bind(f(a), g)) whenever f and g are appropriately measurable.
Русский
Связывание пошагово эквивалентно связыванию в один шаг: bind(bind(m, f), g) = bind(m, a ↦ bind(f(a), g)).
LaTeX
$$$\operatorname{bind}(\operatorname{bind}(m,f), g) = \operatorname{bind}(m, a \mapsto \operatorname{bind}(f(a), g))$$$
Lean4
theorem bind_bind {γ} [MeasurableSpace γ] {m : Measure α} {f : α → Measure β} {g : β → Measure γ}
(hf : AEMeasurable f m) (hg : AEMeasurable g (m.bind f)) : bind (bind m f) g = bind m fun a => bind (f a) g :=
by
ext1 s hs
rw [bind_apply hs hg, lintegral_bind hf, bind_apply hs]
· exact lintegral_congr_ae <| (hf.ae_of_bind hg).mono fun a ha ↦ .symm <| bind_apply hs ha
· exact (aemeasurable_bind hg).comp_aemeasurable hf
· exact (measurable_coe hs).comp_aemeasurable hg
