internlm/Lean-Github huggingface dataset:
Theorem: Probly.flip.arg_x.randFwdDeriv_rule_siple
Proof state before:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx =>
      { val := flip x,
        dval :=
          (fun w dw =>
              let dx' := (fderiv ℝ (fun x => x) w) dw;
              dx' • dflip)
            x dx }) =
    fun x dx => { val := flip x, dval := dx • dflip }
Tactic:
simp
Proof state after:
no goals
Theorem: Probly.randDeriv_const
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.3752
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3869
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3986
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.4109
inst✝ : MeasurableSpace β
a : Rand α
⊢ (randDeriv fun x => a) = fun w dw => 0
Tactic:
funext w dw
Proof state after:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.3752
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3869
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3986
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.4109
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
⊢ randDeriv (fun x => a) w dw = 0
Theorem: Probly.randDeriv_const
Proof state before:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.3752
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3869
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3986
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.4109
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
⊢ randDeriv (fun x => a) w dw = 0
Tactic:
apply DRand.ext
Proof state after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.3752
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3869
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3986
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.4109
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
⊢ ∀ (φ : α → ℝ), (randDeriv (fun x => a) w dw).action φ = 0.action φ
Theorem: Probly.randDeriv_const
Proof state before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.3752
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3869
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3986
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.4109
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
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.3752
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3869
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3986
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.4109
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
φ : α → ℝ
⊢ (randDeriv (fun x => a) w dw).action φ = 0.action φ
Theorem: Probly.randDeriv_const
Proof state before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.3752
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3869
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3986
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.4109
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: Probly.randDeriv_comp
Proof 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
Proof 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
Theorem: Probly.randDeriv_comp
Proof 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
Proof 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
        φ
Theorem: Probly.randDeriv_comp
Proof 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 φ
Proof 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
      φ
Theorem: Probly.randDeriv_comp
Proof 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]
Proof state after:
no goals
Theorem: Probly.Rand.pure.arg_x.randDeriv_rule
Proof 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
Proof 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)
Theorem: Probly.Rand.pure.arg_x.randDeriv_rule
Proof 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
Proof 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 φ
Theorem: Probly.Rand.pure.arg_x.randDeriv_rule
Proof 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 φ
Proof 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 φ
Theorem: Probly.Rand.pure.arg_x.randDeriv_rule
Proof 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]
Proof 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)
Theorem: Probly.Rand.pure.arg_x.randDeriv_rule
Proof 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)
Proof 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)
Theorem: Probly.Rand.pure.arg_x.randDeriv_rule
Proof 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
Proof 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)
Theorem: Probly.Rand.pure.arg_x.randDeriv_rule
Proof 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]
Proof 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)
Theorem: Probly.Rand.pure.arg_x.randDeriv_rule
Proof 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]
Proof state after:
no goals
Theorem: Probly.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
⊢ (randDeriv fun w =>
      let x ~ x w
      f w x) =
    fun w dw =>
    (DRand.bindDR (randDeriv x w dw) fun x => f w x) + bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw
Tactic:
funext w dw
Proof state after:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
w dw : W
⊢ randDeriv
      (fun w =>
        let x ~ x w
        f w x)
      w dw =
    (DRand.bindDR (randDeriv x w dw) fun x => f w x) + bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw