Theorem: log_prod_gaussianPdf
Proof 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]
Proof 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