Theorem: Probly.Rand.bind.arg_xf.randFwdDeriv_rule (Probly/RandFwdDeriv.lean)

State before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.12957
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.13074
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.13191
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
⊢ (randFwdDeriv fun w =>
      let x ~ x w
      f w x) =
    fun w dw =>
    let x ~~ randFwdDeriv x w dw
    randFwdDeriv (fun x_1 => f x_1 x) w dw
Tactic:
unfold randFwdDeriv FDRand.bind
State after:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.12957
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.13074
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.13191
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
⊢ (fun x_1 dx =>
      {
        val :=
          (fun w =>
              let x ~ x w
              f w x)
            x_1,
        dval :=
          randDeriv
            (fun w =>
              let x ~ x w
              f w x)
            x_1 dx }) =
    fun w dw =>
    {
      val :=
        let x' ~ { val := x w, dval := randDeriv x w dw }.val
        ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').val,
      dval :=
        (DRand.bindDR { val := x w, dval := randDeriv x w dw }.dval fun x' =>
            ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').val) +
          bindRD { val := x w, dval := randDeriv x w dw }.val fun x' =>
            ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').dval }

State before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.12957
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.13074
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.13191
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
⊢ (fun x_1 dx =>
      {
        val :=
          (fun w =>
              let x ~ x w
              f w x)
            x_1,
        dval :=
          randDeriv
            (fun w =>
              let x ~ x w
              f w x)
            x_1 dx }) =
    fun w dw =>
    {
      val :=
        let x' ~ { val := x w, dval := randDeriv x w dw }.val
        ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').val,
      dval :=
        (DRand.bindDR { val := x w, dval := randDeriv x w dw }.dval fun x' =>
            ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').val) +
          bindRD { val := x w, dval := randDeriv x w dw }.val fun x' =>
            ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').dval }
Tactic:
simp (disch:=first | apply hx | apply hf) only [rand_simp]
State after:
no goals