Theorem: Probly.Rand.pure.arg_x.randDeriv_rule (Probly/RandDeriv.lean)

State before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
⊢ (randDeriv fun w => pure (x w)) = fun w dw => dpure (x w) ((fderiv ℝ x w) dw)
Tactic:
funext w dw
State after:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ randDeriv (fun w => pure (x w)) w dw = dpure (x w) ((fderiv ℝ x w) dw)

State before:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ randDeriv (fun w => pure (x w)) w dw = dpure (x w) ((fderiv ℝ x w) dw)
Tactic:
apply DRand.ext
State after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ ∀ (φ : X → ℝ), (randDeriv (fun w => pure (x w)) w dw).action φ = (dpure (x w) ((fderiv ℝ x w) dw)).action φ

State before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ ∀ (φ : X → ℝ), (randDeriv (fun w => pure (x w)) w dw).action φ = (dpure (x w) ((fderiv ℝ x w) dw)).action φ
Tactic:
intro φ
State after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
⊢ (randDeriv (fun w => pure (x w)) w dw).action φ = (dpure (x w) ((fderiv ℝ x w) dw)).action φ

State before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
⊢ (randDeriv (fun w => pure (x w)) w dw).action φ = (dpure (x w) ((fderiv ℝ x w) dw)).action φ
Tactic:
simp (disch:=first | assumption | sorry) only
  [randDeriv, pure, Erased.out_mk, integral_dirac', dpure]
State after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
⊢ (fderiv ℝ (fun x' => φ (x x')) w) dw = (fderiv ℝ φ (x w)) ((fderiv ℝ x w) dw)

State before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
⊢ (fderiv ℝ (fun x' => φ (x x')) w) dw = (fderiv ℝ φ (x w)) ((fderiv ℝ x w) dw)
Tactic:
have h := @fderiv.comp ℝ _ _ _ _ _ _ _ _ _ _ x w φ sorry (hx w)
State after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
h : fderiv ℝ (φ ∘ x) w = ContinuousLinearMap.comp (fderiv ℝ φ (x w)) (fderiv ℝ x w)
⊢ (fderiv ℝ (fun x' => φ (x x')) w) dw = (fderiv ℝ φ (x w)) ((fderiv ℝ x w) dw)

State before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
h : fderiv ℝ (φ ∘ x) w = ContinuousLinearMap.comp (fderiv ℝ φ (x w)) (fderiv ℝ x w)
⊢ (fderiv ℝ (fun x' => φ (x x')) w) dw = (fderiv ℝ φ (x w)) ((fderiv ℝ x w) dw)
Tactic:
unfold Function.comp at h
State after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
h : fderiv ℝ (fun x_1 => φ (x x_1)) w = ContinuousLinearMap.comp (fderiv ℝ φ (x w)) (fderiv ℝ x w)
⊢ (fderiv ℝ (fun x' => φ (x x')) w) dw = (fderiv ℝ φ (x w)) ((fderiv ℝ x w) dw)

State before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
h : fderiv ℝ (fun x_1 => φ (x x_1)) w = ContinuousLinearMap.comp (fderiv ℝ φ (x w)) (fderiv ℝ x w)
⊢ (fderiv ℝ (fun x' => φ (x x')) w) dw = (fderiv ℝ φ (x w)) ((fderiv ℝ x w) dw)
Tactic:
rw[h]
State after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
h : fderiv ℝ (fun x_1 => φ (x x_1)) w = ContinuousLinearMap.comp (fderiv ℝ φ (x w)) (fderiv ℝ x w)
⊢ (ContinuousLinearMap.comp (fderiv ℝ φ (x w)) (fderiv ℝ x w)) dw = (fderiv ℝ φ (x w)) ((fderiv ℝ x w) dw)

State before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.21066
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.21183
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.21300
inst✝¹ : MeasurableSpace α
β : Type ?u.21306
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
φ : X → ℝ
h : fderiv ℝ (fun x_1 => φ (x x_1)) w = ContinuousLinearMap.comp (fderiv ℝ φ (x w)) (fderiv ℝ x w)
⊢ (ContinuousLinearMap.comp (fderiv ℝ φ (x w)) (fderiv ℝ x w)) dw = (fderiv ℝ φ (x w)) ((fderiv ℝ x w) dw)
Tactic:
simp only [ContinuousLinearMap.coe_comp', Function.comp_apply]
State after:
no goals