Definitions needed for CvxLean/Examples/CovarianceEstimation.lean.

def Matrix.quadForm {n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : ℝ

Equations

• R.quadForm x = Matrix.dotProduct x (R.mulVec x)

def gaussianPdf {n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : ℝ

Equations

• gaussianPdf R x = 1 / ((2 * Real.pi) ^ n * R.det).sqrt * (-R⁻¹.quadForm x / 2).exp

def covarianceMatrix {N : ℕ} {n : ℕ} (y : Fin N → Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

Equations

• covarianceMatrix y i j = (Finset.univ.sum fun (k : Fin N) => y k i * y k j) / ↑N

theorem gaussianPdf_pos {n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) (y : Fin n → ℝ) (h : R.PosDef) : 0 < gaussianPdf R y

theorem prod_gaussianPdf_pos {N : ℕ} {n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) (y : Fin N → Fin n → ℝ) (h : R.PosDef) : 0 < Finset.univ.prod fun (i : Fin N) => gaussianPdf R (y i)

theorem log_prod_gaussianPdf {N : ℕ} {n : ℕ} (y : Fin N → Fin n → ℝ) (R : Matrix (Fin n) (Fin n) ℝ) (hR : R.PosDef) : (Finset.univ.prod fun (i : Fin N) => gaussianPdf R (y i)).log = Finset.univ.sum fun (i : Fin N) => -(((2 * Real.pi) ^ n).sqrt.log + R.det.sqrt.log) + -R⁻¹.quadForm (y i) / 2

theorem sum_quadForm {n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) {m : ℕ} (y : Fin m → Fin n → ℝ) : (Finset.univ.sum fun (i : Fin m) => R.quadForm (y i)) = ↑m * (covarianceMatrix y * R.transpose).trace

theorem Real.inverse_eq_inv (a : ℝ) : Ring.inverse a = a⁻¹