Theorem: SciLean.dirac.arg_x.parDistribDeriv_rule (SciLean/Core/Distribution/ParametricDistribDeriv.lean)

State before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
⊢ (parDistribDeriv fun w => dirac (x w)) = fun w dw =>
    let xdx := ∂> x w dw;
    diracDeriv xdx.1 xdx.2
Tactic:
funext w dw
State after:
case h.h
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
⊢ parDistribDeriv (fun w => dirac (x w)) w dw =
    let xdx := ∂> x w dw;
    diracDeriv xdx.1 xdx.2

State before:
case h.h
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
⊢ parDistribDeriv (fun w => dirac (x w)) w dw =
    let xdx := ∂> x w dw;
    diracDeriv xdx.1 xdx.2
Tactic:
ext φ
State after:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ (parDistribDeriv (fun w => dirac (x w)) w dw) φ =
    (let xdx := ∂> x w dw;
      diracDeriv xdx.1 xdx.2)
      φ

State before:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ (parDistribDeriv (fun w => dirac (x w)) w dw) φ =
    (let xdx := ∂> x w dw;
      diracDeriv xdx.1 xdx.2)
      φ
Tactic:
unfold parDistribDeriv dirac diracDeriv
State after:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun w => fun φ ⊸[R] φ (x w)) x') φ) φ =
    (let xdx := ∂> x w dw;
      fun φ ⊸[R] ∂ ⇑φ xdx.1 xdx.2)
      φ

State before:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun w => fun φ ⊸[R] φ (x w)) x') φ) φ =
    (let xdx := ∂> x w dw;
      fun φ ⊸[R] ∂ ⇑φ xdx.1 xdx.2)
      φ
Tactic:
simp [pure, fwdDeriv, DistribDifferentiableAt]
State after:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ ∂ (x':=w;dw), φ (x x') = ∂ ⇑φ (x w) (∂ x w dw)

State before:
case h.h.a
R : Type u_1
inst✝⁹ : RealScalar R
W : Type u_2
inst✝⁸ : Vec R W
X : Type u_3
inst✝⁷ : Vec R X
inst✝⁶ : MeasureSpace X
Y : Type ?u.52604
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.53397
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.54186
inst✝¹ : Vec R U
V : Type ?u.54207
inst✝ : Vec R V
x : W → X
hx : CDifferentiable R x
w dw : W
φ : 𝒟 X
⊢ ∂ (x':=w;dw), φ (x x') = ∂ ⇑φ (x w) (∂ x w dw)
Tactic:
fun_trans
State after:
no goals