theorem MeasureTheory.isProbabilityMeasure_bind {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] {f : A → Measure B} [∀ (x : A), IsProbabilityMeasure (f x)] (hf : Measurable f) (μ : Measure A) [IsProbabilityMeasure μ] : IsProbabilityMeasure (μ.bind f)

noncomputable def MeasureTheory.ProbabilityMeasure.bind {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] (μ : ProbabilityMeasure A) (f : A → ProbabilityMeasure B) : ProbabilityMeasure B

Monadic bind for probability measures.

Equations

• μ.bind f = if h : Measurable f then ⟨(↑μ).bind fun (x : A) => ↑(f x), ⋯⟩ else f ⋯.some

theorem MeasureTheory.ProbabilityMeasure.lintegral_bind {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] (μ : ProbabilityMeasure A) {f : A → ProbabilityMeasure B} (hf : Measurable f) {k : B → ENNReal} (hk : Measurable k) : ∫⁻ (x : B), k x ∂↑(μ.bind f) = ∫⁻ (a : A), ∫⁻ (x : B), k x ∂↑(f a) ∂↑μ

theorem MeasureTheory.ProbabilityMeasure.measurable_bind {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] (f : A → ProbabilityMeasure B) : Measurable fun (x : ProbabilityMeasure A) => x.bind f