Rank sublevel sets on the symmetric subspace

The symmetric matrices of rank at most k form a closed, hence measurable, subset of selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ), as the restriction of the closed set of all matrices of rank at most k (Matrix.isClosed_setOfPred_rank_le).

Measurability is what upgrades an everywhere-true rank bound for a symmetric-matrix distribution, such as the Gaussian-Gram Wishart law, to an almost-everywhere statement.

Main declarations

• TauCeti.isClosed_setOfPred_rank_le — the symmetric matrices of rank at most k are closed.
• TauCeti.measurableSet_setOfPred_rank_le — they are measurable.
• TauCeti.measurableSet_setOfPred_rank_eq — exact-rank strata are measurable.

theorem TauCeti.isClosed_setOfPred_rank_le {p : ℕ} (k : ℕ) : IsClosed {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).rank ≤ k}

The symmetric matrices of rank at most k are closed.

theorem TauCeti.measurableSet_setOfPred_rank_le {p : ℕ} (k : ℕ) : MeasurableSet {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).rank ≤ k}

The symmetric matrices of rank at most k are measurable.

theorem TauCeti.measurableSet_setOfPred_rank_eq {p : ℕ} (k : ℕ) : MeasurableSet {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).rank = k}

The symmetric matrices of rank exactly k form a measurable set.