Theorem: Probly.randDeriv_comp (Probly/RandDeriv.lean)

State before:
W : Type ?u.7136
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.7605
inst✝¹ : MeasurableSpace α
β : Type ?u.7611
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
⊢ (randDeriv fun x => f (g x)) = fun x dx =>
    let y := g x;
    let dy := (fderiv ℝ g x) dx;
    randDeriv f y dy
Tactic:
funext x dx
State after:
case h.h
W : Type ?u.7136
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.7605
inst✝¹ : MeasurableSpace α
β : Type ?u.7611
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ randDeriv (fun x => f (g x)) x dx =
    let y := g x;
    let dy := (fderiv ℝ g x) dx;
    randDeriv f y dy

State before:
case h.h
W : Type ?u.7136
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.7605
inst✝¹ : MeasurableSpace α
β : Type ?u.7611
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ randDeriv (fun x => f (g x)) x dx =
    let y := g x;
    let dy := (fderiv ℝ g x) dx;
    randDeriv f y dy
Tactic:
apply DRand.ext
State after:
case h.h.a
W : Type ?u.7136
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.7605
inst✝¹ : MeasurableSpace α
β : Type ?u.7611
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ ∀ (φ : Z → ℝ),
    (randDeriv (fun x => f (g x)) x dx).action φ =
      (let y := g x;
          let dy := (fderiv ℝ g x) dx;
          randDeriv f y dy).action
        φ

State before:
case h.h.a
W : Type ?u.7136
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.7605
inst✝¹ : MeasurableSpace α
β : Type ?u.7611
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ ∀ (φ : Z → ℝ),
    (randDeriv (fun x => f (g x)) x dx).action φ =
      (let y := g x;
          let dy := (fderiv ℝ g x) dx;
          randDeriv f y dy).action
        φ
Tactic:
intro φ
State after:
case h.h.a
W : Type ?u.7136
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.7605
inst✝¹ : MeasurableSpace α
β : Type ?u.7611
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
φ : Z → ℝ
⊢ (randDeriv (fun x => f (g x)) x dx).action φ =
    (let y := g x;
        let dy := (fderiv ℝ g x) dx;
        randDeriv f y dy).action
      φ

State before:
case h.h.a
W : Type ?u.7136
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.7605
inst✝¹ : MeasurableSpace α
β : Type ?u.7611
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
φ : Z → ℝ
⊢ (randDeriv (fun x => f (g x)) x dx).action φ =
    (let y := g x;
        let dy := (fderiv ℝ g x) dx;
        randDeriv f y dy).action
      φ
Tactic:
simp (disch:=first | assumption | apply differentiable_id')
  [randDeriv, deriv_measure_under_integral, fderiv_id', ContinuousLinearMap.coe_id', id_eq]
State after:
no goals