Singular symmetric matrices are Lebesgue-null

The determinant is a polynomial in the upper-triangular coordinates, and it is nonzero because the identity matrix has determinant one. The zero locus of a nonzero polynomial is Lebesgue-null, so the singular symmetric matrices are TauCeti.symmetricLebesgue-null.

This is what makes the degenerate Gaussian-Gram Wishart laws singular with respect to symmetricLebesgue.

Main declarations

• TauCeti.measurableSet_setOfPred_det_eq_zero — the singular matrices are measurable.
• TauCeti.symmetricLebesgue_setOf_det_eq_zero — the singular matrices are symmetricLebesgue-null.

noncomputable def TauCeti.symmetricDetPolynomial (p : ℕ) : MvPolynomial (upperTriangle p) ℝ

The determinant of a symmetric matrix, read through the upper-triangular coordinates as a polynomial.

theorem TauCeti.eval_symmetricDetPolynomial (p : ℕ) (x : upperTriangle p → ℝ) : (MvPolynomial.eval x) (symmetricDetPolynomial p) = (↑((symmetricCoordinates p).symm x)).det

Evaluating the determinant polynomial at a coordinate vector gives the determinant of the symmetric matrix that those coordinates reconstruct.

theorem TauCeti.symmetricDetPolynomial_ne_zero (p : ℕ) : symmetricDetPolynomial p ≠ 0

The determinant polynomial is nonzero, witnessed by the identity matrix, whose determinant is one. This nondegeneracy is what lets the zero-locus theorem apply.

theorem TauCeti.measurableSet_setOfPred_det_eq_zero (p : ℕ) : MeasurableSet {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).det = 0}

The singular symmetric matrices form a closed, hence measurable, set: the determinant is continuous.

theorem TauCeti.symmetricLebesgue_setOf_det_eq_zero (p : ℕ) : (symmetricLebesgue p) {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).det = 0} = 0

The singular symmetric matrices form a symmetricLebesgue-null set.