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

State before:
R : Type u_1
C : Type ?u.21628
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
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ CDifferentiableAt R (fun w => gaussian (μ w) (σ w) (x w)) w
Tactic:
unfold gaussian
State after:
R : Type u_1
C : Type ?u.21628
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
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ CDifferentiableAt R
    (fun w =>
      let x' := (σ w)⁻¹ • (x w - μ w);
      1 / (σ w * Scalar.sqrt (2 * RealScalar.pi)) * Scalar.exp (-‖x'‖₂² / 2))
    w

State before:
R : Type u_1
C : Type ?u.21628
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
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ CDifferentiableAt R
    (fun w =>
      let x' := (σ w)⁻¹ • (x w - μ w);
      1 / (σ w * Scalar.sqrt (2 * RealScalar.pi)) * Scalar.exp (-‖x'‖₂² / 2))
    w
Tactic:
fun_prop (disch:=first | assumption | sorry_proof)
State after:
no goals

State before:
case funProp.discharger
R : Type u_1
C : Type ?u.21628
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
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ σ w ≠ 0
Tactic:
first | assumption | sorry_proof
State after:
no goals

State before:
case funProp.discharger
R : Type u_1
C : Type ?u.21628
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
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ σ w ≠ 0
Tactic:
assumption
State after:
no goals

State before:
case funProp.discharger
R : Type u_1
C : Type ?u.21628
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
σ : W → R
x : W → U
hμ : CDifferentiableAt R μ w
hσ : CDifferentiableAt R σ w
hx : CDifferentiableAt R x w
hσ' : σ w ≠ 0
⊢ 2 ≠ 0
Tactic:
sorry_proof
State after:
no goals