Schoenberg's characterization: the easy direction

Given a real configuration x : Fin n → EuclideanSpace ℝ (Fin k) with squared-distance matrix D, the basepoint-centered Gram matrix centeredGram D is

• positive semidefinite, and
• of rank at most k.

These are exactly the two necessary conditions in Schoenberg's theorem characterizing Euclidean squared-distance matrices. The converse (sufficiency) is proved in SchoenbergHard.lean.

The proof goes through the polarization identity centeredGram D i j = ⟪x i - x 0, x j - x 0⟫, exhibiting centeredGram D as the Gram matrix of the recentred vectors x i - x 0. Positive semidefiniteness is then Matrix.posSemidef_gram; the rank bound comes from the factorization gram = mᴴ * m over the standard orthonormal basis of EuclideanSpace ℝ (Fin k) together with Matrix.rank_conjTranspose_mul_self and Matrix.rank_le_card_height.

Main results

• DistanceGeometry.centeredGram_apply_eq_inner : the polarization identity.
• DistanceGeometry.centeredGram_eq_gram : centeredGram D is a Gram matrix.
• DistanceGeometry.posSemidef_centeredGram, DistanceGeometry.rank_centeredGram_le, DistanceGeometry.schoenberg_easy : the necessary conditions.

theorem DistanceGeometry.centeredGram_apply_eq_inner {n k : ℕ} [NeZero n] {D : Matrix (Fin n) (Fin n) ℝ} {x : Fin n → EuclideanSpace ℝ (Fin k)} (hD : IsSqDistMatrix D x) (i j : Fin n) : centeredGram D i j = inner ℝ (x i - x 0) (x j - x 0)

The polarization identity. When D is the squared-distance matrix of x, the (i, j) entry of the basepoint-centered Gram matrix is the inner product of the recentred vectors x i - x 0 and x j - x 0.

theorem DistanceGeometry.centeredGram_eq_gram {n k : ℕ} [NeZero n] {D : Matrix (Fin n) (Fin n) ℝ} {x : Fin n → EuclideanSpace ℝ (Fin k)} (hD : IsSqDistMatrix D x) : centeredGram D = Matrix.gram ℝ fun (i : Fin n) => x i - x 0

The basepoint-centered Gram matrix is the Gram matrix of the recentred vectors.

theorem DistanceGeometry.posSemidef_centeredGram {n k : ℕ} [NeZero n] {D : Matrix (Fin n) (Fin n) ℝ} {x : Fin n → EuclideanSpace ℝ (Fin k)} (hD : IsSqDistMatrix D x) : (centeredGram D).PosSemidef

The basepoint-centered Gram matrix of a squared-distance matrix is positive semidefinite. This is the positive-semidefiniteness half of Schoenberg's necessary conditions.

theorem DistanceGeometry.rank_centeredGram_le {n k : ℕ} [NeZero n] {D : Matrix (Fin n) (Fin n) ℝ} {x : Fin n → EuclideanSpace ℝ (Fin k)} (hD : IsSqDistMatrix D x) : (centeredGram D).rank ≤ k

The basepoint-centered Gram matrix of a squared-distance matrix of a configuration in dimension k has rank at most k. This is the rank half of Schoenberg's necessary conditions.

theorem DistanceGeometry.schoenberg_easy {n k : ℕ} [NeZero n] {D : Matrix (Fin n) (Fin n) ℝ} {x : Fin n → EuclideanSpace ℝ (Fin k)} (hD : IsSqDistMatrix D x) : (centeredGram D).PosSemidef ∧ (centeredGram D).rank ≤ k

The necessary conditions in Schoenberg's theorem: the basepoint-centered Gram matrix of a squared-distance matrix of a configuration in EuclideanSpace ℝ (Fin k) is positive semidefinite and has rank at most k.