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

State before:
R : Type u_1
C : Type ?u.17313
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
μ : W → U
σ : R
x : W → U
hμ : CDifferentiable R μ
hx : CDifferentiable R x
⊢ CDifferentiable R fun w => gaussian (μ w) σ (x w)
Tactic:
intro w
State after:
R : Type u_1
C : Type ?u.17313
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
μ : W → U
σ : R
x : W → U
hμ : CDifferentiable R μ
hx : CDifferentiable R x
w : W
⊢ CDifferentiableAt R (fun w => gaussian (μ w) σ (x w)) w

State before:
R : Type u_1
C : Type ?u.17313
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type u_2
inst✝¹ : Vec R W
U : Type u_3
inst✝ : SemiHilbert R U
μ : W → U
σ : R
x : W → U
hμ : CDifferentiable R μ
hx : CDifferentiable R x
w : W
⊢ CDifferentiableAt R (fun w => gaussian (μ w) σ (x w)) w
Tactic:
fun_prop
State after:
no goals