Theorem: SciLean.cintegral.arg_f.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_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
⊢ (parDistribDeriv fun w => ↑fun x => ∫' y, f w x y) = fun w dw =>
    let Tf := fun w => ↑fun x => ↑fun y => f w x y;
    postComp (parDistribDeriv Tf w dw) (fun T ⊸[R] ⟪T, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z])
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_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
⊢ parDistribDeriv (fun w => ↑fun x => ∫' y, f w x y) w dw =
    let Tf := fun w => ↑fun x => ↑fun y => f w x y;
    postComp (parDistribDeriv Tf w dw) (fun T ⊸[R] ⟪T, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z])

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_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
⊢ parDistribDeriv (fun w => ↑fun x => ∫' y, f w x y) w dw =
    let Tf := fun w => ↑fun x => ↑fun y => f w x y;
    postComp (parDistribDeriv Tf w dw) (fun T ⊸[R] ⟪T, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z])
Tactic:
unfold parDistribDeriv postComp Function.toDistribution
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_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun w => fun φ ⊸[R] ∫' x, φ x • (fun x => ∫' y, f w x y) x) x') φ) =
    let Tf := fun w => fun φ ⊸[R] ∫' x, φ x • (fun x => fun φ ⊸[R] ∫' x_1, φ x_1 • (fun y => f w x y) x_1) x;
    fun φ ⊸[R] (fun T ⊸[R] ⟪T, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z]) ((fun φ ⊸ ∂ (x':=w;dw), (Tf x') φ) φ)

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_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun w => fun φ ⊸[R] ∫' x, φ x • (fun x => ∫' y, f w x y) x) x') φ) =
    let Tf := fun w => fun φ ⊸[R] ∫' x, φ x • (fun x => fun φ ⊸[R] ∫' x_1, φ x_1 • (fun y => f w x y) x_1) x;
    fun φ ⊸[R] (fun T ⊸[R] ⟪T, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z]) ((fun φ ⊸ ∂ (x':=w;dw), (Tf x') φ) φ)
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_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun w => fun φ ⊸[R] ∫' x, φ x • (fun x => ∫' y, f w x y) x) x') φ) φ =
    (let Tf := fun w => fun φ ⊸[R] ∫' x, φ x • (fun x => fun φ ⊸[R] ∫' x_1, φ x_1 • (fun y => f w x y) x_1) x;
      fun φ ⊸[R] (fun T ⊸[R] ⟪T, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z]) ((fun φ ⊸ ∂ (x':=w;dw), (Tf x') φ) φ))
      φ

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_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun w => fun φ ⊸[R] ∫' x, φ x • (fun x => ∫' y, f w x y) x) x') φ) φ =
    (let Tf := fun w => fun φ ⊸[R] ∫' x, φ x • (fun x => fun φ ⊸[R] ∫' x_1, φ x_1 • (fun y => f w x y) x_1) x;
      fun φ ⊸[R] (fun T ⊸[R] ⟪T, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z]) ((fun φ ⊸ ∂ (x':=w;dw), (Tf x') φ) φ))
      φ
Tactic:
simp [ftrans_simp]
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_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
φ : 𝒟 X
⊢ ∂ (x':=w;dw), ∫' x, φ x • ∫' y, f x' x y =
    ⟪∂ (x':=w;dw), ∫' x, φ x • fun φ ⊸[R] ∫' x_1, φ x_1 • f x' x x_1, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z]

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_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
φ : 𝒟 X
⊢ ∂ (x':=w;dw), ∫' x, φ x • ∫' y, f x' x y =
    ⟪∂ (x':=w;dw), ∫' x, φ x • fun φ ⊸[R] ∫' x_1, φ x_1 • f x' x x_1, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z]
Tactic:
sorry_proof
State after:
no goals