Theorem: SciLean.Prob.Rand.lintegral_bind (SciLean/Modules/Prob/Rand.lean)

State before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.5407
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
φ : Y → ℝ≥0∞
hf : Measurable f
hφ : Measurable φ
⊢ ∫⁻ (x' : Y), φ x' ∂↑(bind x f).μ = ∫⁻ (x' : X), ∫⁻ (y' : Y), φ y' ∂↑(f x').μ ∂↑x.μ
Tactic:
simp [bind]
State after:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.5407
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
φ : Y → ℝ≥0∞
hf : Measurable f
hφ : Measurable φ
⊢ (∫⁻ (x' : Y), φ x' ∂Measure.bind ↑x.μ fun x => ↑(f x).μ) = ∫⁻ (x' : X), ∫⁻ (x' : Y), φ x' ∂↑(f x').μ ∂↑x.μ

State before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.5407
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
φ : Y → ℝ≥0∞
hf : Measurable f
hφ : Measurable φ
⊢ (∫⁻ (x' : Y), φ x' ∂Measure.bind ↑x.μ fun x => ↑(f x).μ) = ∫⁻ (x' : X), ∫⁻ (x' : Y), φ x' ∂↑(f x').μ ∂↑x.μ
Tactic:
apply Measure.lintegral_bind (is_measurable hf) hφ
State after:
no goals