Theorem: SciLean.Prob.distribFwdDeriv_comp (SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean)

State before:
W : Type u_1
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_3
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u_2
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f : Y → Distribution Z
g : X → Y
x dx : X
φ : Z → W × W
hf : DistribDifferentiable f
hg : DifferentiableAt ℝ g x
⊢ ⟪distribFwdDeriv (fun x => f (g x)) x dx, φ⟫ =
    let ydy := fwdFDeriv ℝ g x dx;
    ⟪distribFwdDeriv f ydy.1 ydy.2, φ⟫
Tactic:
simp (disch := assumption) only [action, distribFwdDeriv, fwdFDeriv]
State after:
W : Type u_1
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_3
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u_2
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f : Y → Distribution Z
g : X → Y
x dx : X
φ : Z → W × W
hf : DistribDifferentiable f
hg : DifferentiableAt ℝ g x
⊢ ((f (g x)).action fun x => (φ x).1,
      ((distribDeriv (fun x => f (g x)) x dx).action fun x => (φ x).1) + (f (g x)).action fun x => (φ x).2) =
    ((f (g x)).action fun x => (φ x).1,
      ((distribDeriv f (g x) ((fderiv ℝ g x) dx)).action fun x => (φ x).1) + (f (g x)).action fun x => (φ x).2)

State before:
W : Type u_1
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_3
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u_2
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f : Y → Distribution Z
g : X → Y
x dx : X
φ : Z → W × W
hf : DistribDifferentiable f
hg : DifferentiableAt ℝ g x
⊢ ((f (g x)).action fun x => (φ x).1,
      ((distribDeriv (fun x => f (g x)) x dx).action fun x => (φ x).1) + (f (g x)).action fun x => (φ x).2) =
    ((f (g x)).action fun x => (φ x).1,
      ((distribDeriv f (g x) ((fderiv ℝ g x) dx)).action fun x => (φ x).1) + (f (g x)).action fun x => (φ x).2)
Tactic:
simp (disch := assumption) only [distribution_action_normalize, distribDeriv_comp]
State after:
no goals