Schoenberg's characterization: the sufficiency direction

This file proves the converse of schoenberg_easy: if D satisfies IsPreDistMatrix, this project's symmetric-and-hollow structural predicate, and its basepoint-centered Gram matrix is positive semidefinite of rank at most k, then D is the squared-distance matrix of some configuration in EuclideanSpace ℝ (Fin k). Combined with the easy direction this gives the full Schoenberg characterization schoenberg.

The mathematical core is a rank-controlled factorization of a positive semidefinite matrix, Matrix.PosSemidef.exists_conjTranspose_mul_self_of_rank_le, which states that a PSD matrix G with G.rank ≤ k factors as Mᴴ * M for some k × n matrix M. This is proved from the spectral theorem (a full factorization Nᴴ * N = G with N = diagonal (√eigenvalues) * Uᴴ) followed by relocating the support of the nonzero eigenvalues into Fin k via a scatter matrix. Given such an M, the columns of M, viewed in EuclideanSpace ℝ (Fin k), realize the configuration, and reverse polarization recovers D.

Main results

• Matrix.PosSemidef.exists_conjTranspose_mul_self_of_rank_le : rank-controlled Cholesky-type factorization of a PSD matrix.
• DistanceGeometry.schoenberg_hard : the sufficiency direction.
• DistanceGeometry.schoenberg : the full characterization (an iff).

Rank-controlled factorization of a positive semidefinite matrix

Scatter matrix: relocate the support into Fin k

The k × n factor M with Mᴴ * M = G

theorem Matrix.PosSemidef.exists_conjTranspose_mul_self_of_rank_le {n k : ℕ} {G : Matrix (Fin n) (Fin n) ℝ} (hG : G.PosSemidef) (hrank : G.rank ≤ k) : ∃ (M : Matrix (Fin k) (Fin n) ℝ), M.conjTranspose * M = G

A positive semidefinite matrix G with G.rank ≤ k factors as Mᴴ * M for some matrix M : Matrix (Fin k) (Fin n) ℝ. This rank-controlled Cholesky-type factorization realizes G in ambient dimension k and uses only G.rank active directions.

Schoenberg, sufficiency direction

theorem DistanceGeometry.schoenberg_hard {n k : ℕ} [NeZero n] {D : Matrix (Fin n) (Fin n) ℝ} (hD : IsPreDistMatrix D) (hPSD : (centeredGram D).PosSemidef) (hrank : (centeredGram D).rank ≤ k) : EmbedsIn D k

The sufficiency direction of Schoenberg's theorem. If D satisfies this project's IsPreDistMatrix predicate (symmetric and hollow) and its basepoint-centered Gram matrix is positive semidefinite of rank at most k, then D is the squared-distance matrix of some configuration in EuclideanSpace ℝ (Fin k).

This is the converse of schoenberg_easy: it reconstructs the point configuration from the Gram data.

theorem DistanceGeometry.schoenberg {n k : ℕ} [NeZero n] {D : Matrix (Fin n) (Fin n) ℝ} (hD : IsPreDistMatrix D) : EmbedsIn D k ↔ (centeredGram D).PosSemidef ∧ (centeredGram D).rank ≤ k

Schoenberg's characterization of Euclidean squared-distance matrices. A matrix D satisfying this project's IsPreDistMatrix predicate (symmetric and hollow) embeds as a squared-distance matrix in EuclideanSpace ℝ (Fin k) if and only if its basepoint-centered Gram matrix is positive semidefinite and has rank at most k.