Theorem: SciLean.Rand.bind_pdf (SciLean/Core/Rand/Rand.lean)

State before:
X Y : Type
Z : Type ?u.124691
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
R : Type u_1
inst✝² : RealScalar R
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
ν : Measure Y
x : Rand X
f : X → Rand Y
⊢ pdf R (x >>= f) ν = fun y => ∫ (x' : X), pdf R (f x') ν y ∂x.ℙ
Tactic:
funext y
State after:
case h
X Y : Type
Z : Type ?u.124691
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
R : Type u_1
inst✝² : RealScalar R
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf R (x >>= f) ν y = ∫ (x' : X), pdf R (f x') ν y ∂x.ℙ

State before:
case h
X Y : Type
Z : Type ?u.124691
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
R : Type u_1
inst✝² : RealScalar R
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf R (x >>= f) ν y = ∫ (x' : X), pdf R (f x') ν y ∂x.ℙ
Tactic:
simp[Rand.pdf,Bind.bind,Pure.pure]
State after:
case h
X Y : Type
Z : Type ?u.124691
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
R : Type u_1
inst✝² : RealScalar R
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ Scalar.ofReal R
      ({ spec := erase fun φ => Erased.out x.spec fun x => Erased.out (f x).spec φ,
                rand := StateT.bind x.rand fun x => (f x).rand }.ℙ.rnDeriv
          ν y).toReal =
    ∫ (x' : X), Scalar.ofReal R ((f x').ℙ.rnDeriv ν y).toReal ∂x.ℙ

State before:
case h
X Y : Type
Z : Type ?u.124691
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
R : Type u_1
inst✝² : RealScalar R
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ Scalar.ofReal R
      ({ spec := erase fun φ => Erased.out x.spec fun x => Erased.out (f x).spec φ,
                rand := StateT.bind x.rand fun x => (f x).rand }.ℙ.rnDeriv
          ν y).toReal =
    ∫ (x' : X), Scalar.ofReal R ((f x').ℙ.rnDeriv ν y).toReal ∂x.ℙ
Tactic:
sorry_proof
State after:
no goals