Theorem: SciLean.gaussian.arg_μx.CDifferentiableAt_rule (SciLean/Core/Functions/Gaussian.lean)

State before:
R : Type u_1
C : Type ?u.15871
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : R
x : W → U
hμ : CDifferentiableAt R μ w
hx : CDifferentiableAt R x w
⊢ CDifferentiableAt R (fun w => gaussian (μ w) σ (x w)) w
Tactic:
unfold gaussian
State after:
R : Type u_1
C : Type ?u.15871
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : R
x : W → U
hμ : CDifferentiableAt R μ w
hx : CDifferentiableAt R x w
⊢ CDifferentiableAt R
    (fun w =>
      let x' := σ⁻¹ • (x w - μ w);
      1 / (σ * Scalar.sqrt (2 * RealScalar.pi)) * Scalar.exp (-‖x'‖₂² / 2))
    w

State before:
R : Type u_1
C : Type ?u.15871
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
w : W
μ : W → U
σ : R
x : W → U
hμ : CDifferentiableAt R μ w
hx : CDifferentiableAt R x w
⊢ CDifferentiableAt R
    (fun w =>
      let x' := σ⁻¹ • (x w - μ w);
      1 / (σ * Scalar.sqrt (2 * RealScalar.pi)) * Scalar.exp (-‖x'‖₂² / 2))
    w
Tactic:
fun_prop
State after:
no goals