Theorem: SciLean.Prob.FDRand.expectedValueAndChange_as_fdmean (SciLean/Modules/Prob/FDRand.lean)

State before:
R : Type ?u.45469
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
φ : X → Y
⊢ fdE x φ =
    fdmean
      (let x' ~~ x
      fdpure (φ x') 0)
Tactic:
simp (disch:=sorry) only [rand_simp,mean,fdE,fdmean,bind,fdpure,id]
State after:
R : Type ?u.45469
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
φ : X → Y
⊢ (E x.val φ, DRand.dE x.dval φ) =
    (E
        (let x' ~ x.val
        Rand.pure (φ x'))
        id,
      (DRand.dE x.dval fun x' => φ x') + E x.val fun x' => (fderiv ℝ id (φ x')) 0)

State before:
R : Type ?u.45469
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
φ : X → Y
⊢ (E x.val φ, DRand.dE x.dval φ) =
    (E
        (let x' ~ x.val
        Rand.pure (φ x'))
        id,
      (DRand.dE x.dval fun x' => φ x') + E x.val fun x' => (fderiv ℝ id (φ x')) 0)
Tactic:
simp
State after:
no goals