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

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
⊢ (∏ i : Fin N, gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Tactic:
have : ∀ i,
  i ∈ Finset.univ → gaussianPdf R (y i) ≠ 0 := fun i _ => ne_of_gt (gaussianPdf_pos _ _ hR)
State after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ (∏ i : Fin N, gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ (∏ i : Fin N, gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Tactic:
have sqrt_2_pi_n_R_det_ne_zero: sqrt ((2 * π) ^ n * R.det) ≠ 0 := by
  refine' ne_of_gt (sqrt_pos.2 (mul_pos _ hR.det_pos))
  exact (pow_pos (mul_pos (by positivity) pi_pos) _)
State after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ (∏ i : Fin N, gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ (∏ i : Fin N, gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Tactic:
rw [log_prod Finset.univ (fun i => gaussianPdf R (y i)) this]
State after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ ∑ i : Fin N, (gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ ∑ i : Fin N, (gaussianPdf R (y i)).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Tactic:
unfold gaussianPdf
State after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ ∑ i : Fin N, (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ ∑ i : Fin N, (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log =
    ∑ i : Fin N, (-(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2)
Tactic:
apply congr_arg (Finset.sum Finset.univ)
State after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ (fun i => (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log) = fun i =>
    -(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
⊢ (fun i => (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log) = fun i =>
    -(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2
Tactic:
ext i
State after:
case h
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log =
    -(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2

State before:
case h
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (1 / ((2 * π) ^ n * R.det).sqrt * (-R⁻¹.quadForm (y i) / 2).exp).log =
    -(((2 * π) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2
Tactic:
rw [log_mul, log_div, sqrt_mul, log_mul, log_exp, log_one, zero_sub]
State after:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ R.det.sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0

State before:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ R.det.sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
simp [rpow_eq_pow]
State after:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ¬((2 * π) ^ n).sqrt = 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ R.det.sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0

State before:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ¬((2 * π) ^ n).sqrt = 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ R.det.sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact ne_of_gt (sqrt_pos.2 (pow_pos (mul_pos (by positivity) pi_pos) _))
State after:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ R.det.sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0

State before:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ R.det.sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact ne_of_gt (sqrt_pos.2 hR.det_pos)
State after:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0

State before:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ (2 * π) ^ n

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact pow_nonneg (mul_nonneg (by positivity) (le_of_lt pi_pos)) _
State after:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0

State before:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
norm_num
State after:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0

State before:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact sqrt_2_pi_n_R_det_ne_zero
State after:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0

State before:
case h.hx
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 / ((2 * π) ^ n * R.det).sqrt ≠ 0

case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact div_ne_zero (by norm_num) sqrt_2_pi_n_R_det_ne_zero
State after:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0

State before:
case h.hy
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ (-R⁻¹.quadForm (y i) / 2).exp ≠ 0
Tactic:
exact exp_ne_zero _
State after:
no goals

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ ((2 * π) ^ n * R.det).sqrt ≠ 0
Tactic:
refine' ne_of_gt (sqrt_pos.2 (mul_pos _ hR.det_pos))
State after:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ 0 < (2 * π) ^ n

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ 0 < (2 * π) ^ n
Tactic:
exact (pow_pos (mul_pos (by positivity) pi_pos) _)
State after:
no goals

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
⊢ 0 < 2
Tactic:
positivity
State after:
no goals

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 < 2
Tactic:
positivity
State after:
no goals

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 0 ≤ 2
Tactic:
positivity
State after:
no goals

State before:
N n : ℕ
y : Fin N → Fin n → ℝ
R : Matrix (Fin n) (Fin n) ℝ
hR : R.PosDef
this : ∀ i ∈ Finset.univ, gaussianPdf R (y i) ≠ 0
sqrt_2_pi_n_R_det_ne_zero : ((2 * π) ^ n * R.det).sqrt ≠ 0
i : Fin N
⊢ 1 ≠ 0
Tactic:
norm_num
State after:
no goals