Theorem: gaussianPdf_pos (CvxLean/Lib/Math/CovarianceEstimation.lean)

State before:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
y : Fin n → ℝ
h : R.PosDef
⊢ 0 < gaussianPdf R y
Tactic:
refine' mul_pos (div_pos zero_lt_one (sqrt_pos.2 (mul_pos _ h.det_pos))) (exp_pos _)
State after:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
y : Fin n → ℝ
h : R.PosDef
⊢ 0 < (2 * π) ^ n

State before:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
y : Fin n → ℝ
h : R.PosDef
⊢ 0 < (2 * π) ^ n
Tactic:
exact (pow_pos (mul_pos (by positivity) pi_pos) n)
State after:
no goals

State before:
n : ℕ
R : Matrix (Fin n) (Fin n) ℝ
y : Fin n → ℝ
h : R.PosDef
⊢ 0 < 2
Tactic:
positivity
State after:
no goals