Almost-sure rank of matrices with a density

A rectangular real matrix sampled from a law absolutely continuous with respect to product Lebesgue measure has maximal rank almost surely. More precisely, each fixed square submatrix selected by embeddings has nonzero determinant almost surely. The determinant polynomial is Mathlib's Matrix.mvPolynomialX, renamed along the selected coordinates; its zero locus is null by MvPolynomial.volume_setOfPred_eval_eq_zero.

These results apply to matrices with dependent entries as well as independent ones, provided the joint law has a density. Empty row, column, and minor index types are allowed.

The exact-rank strata are measurable, and the maximal-rank conclusion is available both for function-valued arrays and for the bundled Matrix type.

theorem Matrix.measurableSet_setOfPred_rank_eq {m : Type u_1} {n : Type u_2} [Finite m] [Fintype n] (k : ℕ) : MeasurableSet {A : Matrix m n ℝ | A.rank = k}

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

theorem MeasureTheory.Measure.ae_det_submatrix_ne_zero {m : Type u_1} {n : Type u_2} {l : Type u_3} [Fintype m] [Fintype n] [Fintype l] [DecidableEq l] (μ : Measure (m → n → ℝ)) (hμ : μ.AbsolutelyContinuous volume) (r : l ↪ m) (c : l ↪ n) : ∀ᵐ (A : m → n → ℝ) ∂μ, ((Matrix.of A).submatrix ⇑r ⇑c).det ≠ 0

Every fixed square minor of a real matrix with an absolutely continuous law is nonzero almost surely. The row and column embeddings need not preserve any ordering.

theorem MeasureTheory.Measure.ae_rank_eq_min {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (μ : Measure (m → n → ℝ)) (hμ : μ.AbsolutelyContinuous volume) : ∀ᵐ (A : m → n → ℝ) ∂μ, (Matrix.of A).rank = min (Fintype.card m) (Fintype.card n)

A rectangular real matrix whose law is absolutely continuous with respect to product Lebesgue measure has maximal rank almost surely, including when one index type is empty.

theorem MeasureTheory.Measure.ae_rank_eq_min_matrix {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (μ : Measure (Matrix m n ℝ)) (hμ : μ.AbsolutelyContinuous volume) : ∀ᵐ (X : Matrix m n ℝ) ∂μ, X.rank = min (Fintype.card m) (Fintype.card n)

A real matrix whose law is absolutely continuous with respect to product Lebesgue measure has maximal rank almost surely, including when one index type is empty.