Theorem: SciLean.log_gaussian (SciLean/Core/Functions/Gaussian.lean)

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

State before:
R : Type u_1
C : Type ?u.4719
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.4729
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiHilbert R U
μ : U
σ : R
x : U
⊢ log
      (let x' := σ⁻¹ • (x - μ);
      1 / (σ * sqrt (2 * pi)) * exp (-‖x'‖₂² / 2)) =
    let x' := σ⁻¹ • (x - μ);
    -‖x'‖₂² / 2 - log σ - log (sqrt (2 * pi))
Tactic:
simp [log_inv,log_mul,log_div,log_exp,log_one]
State after:
R : Type u_1
C : Type ?u.4719
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.4729
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiHilbert R U
μ : U
σ : R
x : U
⊢ -log (sqrt (2 * pi)) + -log σ + -‖σ⁻¹ • (x - μ)‖₂² / 2 = -‖σ⁻¹ • (x - μ)‖₂² / 2 - log σ - log (sqrt (2 * pi))

State before:
R : Type u_1
C : Type ?u.4719
inst✝³ : Scalar R C
inst✝² : RealScalar R
W : Type ?u.4729
inst✝¹ : Vec R W
U : Type u_2
inst✝ : SemiHilbert R U
μ : U
σ : R
x : U
⊢ -log (sqrt (2 * pi)) + -log σ + -‖σ⁻¹ • (x - μ)‖₂² / 2 = -‖σ⁻¹ • (x - μ)‖₂² / 2 - log σ - log (sqrt (2 * pi))
Tactic:
ring
State after:
no goals