internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Prob.randDeriv_const
Proof state before:
case h.h.a
R : Type ?u.4672
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.4928
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.5167
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.5406
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.5651
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
⊢ ∀ (φ : α → ℝ), (randDeriv (fun x => a) w dw).action φ = 0.action φ
Tactic:
intro φ
Proof state after:
case h.h.a
R : Type ?u.4672
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.4928
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.5167
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.5406
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.5651
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
φ : α → ℝ
⊢ (randDeriv (fun x => a) w dw).action φ = 0.action φ
Theorem: SciLean.Prob.randDeriv_const
Proof state before:
case h.h.a
R : Type ?u.4672
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.4928
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.5167
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.5406
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.5651
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
φ : α → ℝ
⊢ (randDeriv (fun x => a) w dw).action φ = 0.action φ
Tactic:
simp only [randDeriv, fderiv_const, Pi.zero_apply,
           ContinuousLinearMap.zero_apply, DRand.action_zero]
Proof state after:
no goals
Theorem: SciLean.Prob.randDeriv_comp
Proof state before:
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
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 ydy := fwdFDeriv ℝ g x dx;
    randDeriv f ydy.1 ydy.2
Tactic:
funext x dx
Proof state after:
case h.h
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
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 ydy := fwdFDeriv ℝ g x dx;
    randDeriv f ydy.1 ydy.2
Theorem: SciLean.Prob.randDeriv_comp
Proof state before:
case h.h
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
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 ydy := fwdFDeriv ℝ g x dx;
    randDeriv f ydy.1 ydy.2
Tactic:
unfold fwdFDeriv
Proof state after:
case h.h
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
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 ydy := (g x, (fderiv ℝ g x) dx);
    randDeriv f ydy.1 ydy.2
Theorem: SciLean.Prob.randDeriv_comp
Proof state before:
case h.h
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
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 ydy := (g x, (fderiv ℝ g x) dx);
    randDeriv f ydy.1 ydy.2
Tactic:
apply DRand.ext
Proof state after:
case h.h.a
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
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 ydy := (g x, (fderiv ℝ g x) dx);
          randDeriv f ydy.1 ydy.2).action
        φ
Theorem: SciLean.Prob.randDeriv_comp
Proof state before:
case h.h.a
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
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 ydy := (g x, (fderiv ℝ g x) dx);
          randDeriv f ydy.1 ydy.2).action
        φ
Tactic:
intro φ
Proof state after:
case h.h.a
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
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 ydy := (g x, (fderiv ℝ g x) dx);
        randDeriv f ydy.1 ydy.2).action
      φ
Theorem: SciLean.Prob.randDeriv_comp
Proof state before:
case h.h.a
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
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 ydy := (g x, (fderiv ℝ g x) dx);
        randDeriv f ydy.1 ydy.2).action
      φ
Tactic:
simp (disch:=first | assumption | apply differentiable_id')
  [randDeriv, deriv_measure_under_integral, fderiv_id', ContinuousLinearMap.coe_id', id_eq]
Proof state after:
no goals
Theorem: SciLean.Prob.Rand.pure.arg_x.randDeriv_rule
Proof state before:
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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
Proof state after:
case h.h
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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)
Theorem: SciLean.Prob.Rand.pure.arg_x.randDeriv_rule
Proof state before:
case h.h
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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
Proof state after:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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 φ
Theorem: SciLean.Prob.Rand.pure.arg_x.randDeriv_rule
Proof state before:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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 φ
Proof state after:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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 φ
Theorem: SciLean.Prob.Rand.pure.arg_x.randDeriv_rule
Proof state before:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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]
Proof state after:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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)
Theorem: SciLean.Prob.Rand.pure.arg_x.randDeriv_rule
Proof state before:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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)
Proof state after:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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)
Theorem: SciLean.Prob.Rand.pure.arg_x.randDeriv_rule
Proof state before:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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
Proof state after:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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)
Theorem: SciLean.Prob.Rand.pure.arg_x.randDeriv_rule
Proof state before:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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]
Proof state after:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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)
Theorem: SciLean.Prob.Rand.pure.arg_x.randDeriv_rule
Proof state before:
case h.h.a
R : Type ?u.22279
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.22774
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.23013
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.23252
inst✝¹ : MeasurableSpace α
β : Type ?u.23258
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]
Proof state after:
no goals