Theorem: SciLean.parDistribRevDeriv.dirac.arg_xy.parDistribRevDeriv_rule (SciLean/Core/Distribution/ParametricDistribRevDeriv.lean)

State before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
⊢ (parDistribRevDeriv fun w => dirac (x w)) = fun w =>
    let xdx := revDeriv' R x w;
    postComp (diracRevDeriv xdx.1)
      (fun x ⊸
        match x with
        | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr)))
Tactic:
funext w
State after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
⊢ parDistribRevDeriv (fun w => dirac (x w)) w =
    let xdx := revDeriv' R x w;
    postComp (diracRevDeriv xdx.1)
      (fun x ⊸
        match x with
        | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr)))

State before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
⊢ parDistribRevDeriv (fun w => dirac (x w)) w =
    let xdx := revDeriv' R x w;
    postComp (diracRevDeriv xdx.1)
      (fun x ⊸
        match x with
        | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr)))
Tactic:
apply Distribution.ext _ _
State after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
⊢ ∀ (φ : 𝒟 X),
    (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
      (let xdx := revDeriv' R x w;
        postComp (diracRevDeriv xdx.1)
          (fun x ⊸
            match x with
            | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
        φ

State before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
⊢ ∀ (φ : 𝒟 X),
    (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
      (let xdx := revDeriv' R x w;
        postComp (diracRevDeriv xdx.1)
          (fun x ⊸
            match x with
            | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
        φ
Tactic:
intro φ
State after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
⊢ (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
    (let xdx := revDeriv' R x w;
      postComp (diracRevDeriv xdx.1)
        (fun x ⊸
          match x with
          | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
      φ

State before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
⊢ (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
    (let xdx := revDeriv' R x w;
      postComp (diracRevDeriv xdx.1)
        (fun x ⊸
          match x with
          | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
      φ
Tactic:
have : HasAdjDiff R φ := sorry_proof
State after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
this : HasAdjDiff R ⇑φ
⊢ (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
    (let xdx := revDeriv' R x w;
      postComp (diracRevDeriv xdx.1)
        (fun x ⊸
          match x with
          | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
      φ

State before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
this : HasAdjDiff R ⇑φ
⊢ (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
    (let xdx := revDeriv' R x w;
      postComp (diracRevDeriv xdx.1)
        (fun x ⊸
          match x with
          | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
      φ
Tactic:
simp [diracRevDeriv,revDeriv, parDistribRevDeriv, postComp]
State after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
this : HasAdjDiff R ⇑φ
⊢ (fun dz ⊸[R] semiAdjoint R (fun dx => ∂ (x_1:=w;dx), φ (x x_1)) dz) =
    fun dr ⊸[R] semiAdjoint R (∂ x w) (semiAdjoint R (∂ ⇑φ (x w)) dr)

State before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
this : HasAdjDiff R ⇑φ
⊢ (fun dz ⊸[R] semiAdjoint R (fun dx => ∂ (x_1:=w;dx), φ (x x_1)) dz) =
    fun dr ⊸[R] semiAdjoint R (∂ x w) (semiAdjoint R (∂ ⇑φ (x w)) dr)
Tactic:
sorry_proof
State after:
no goals