aemeasurable_bind — Mathlib

English

If g is almost everywhere measurable with respect to m.join, then the map m ↦ bind m g is almost everywhere measurable with respect to m.

Русский

Если g измерима практически всюду относительно m.join, то m ↦ bind m g измеримо почти везде относительно m.

LaTeX

$$$AEMeasurable(g, m.join) \Rightarrow AEMeasurable(\lambda x. x \bind g, m)$$$

Lean4

theorem aemeasurable_bind {g : α → Measure β} {m : Measure (Measure α)} (hg : AEMeasurable g m.join) :
    AEMeasurable (bind · g) m :=
  let ⟨f, hfm, hf⟩ := hg
  ⟨(bind · f), measurable_bind' hfm, (ae_ae_of_ae_join hf).mono fun _ ↦ bind_congr_right⟩

Похожие утверждения