Distance geometry: core definitions

This file sets up the basic objects of Euclidean distance geometry: the squared-distance matrix of a point configuration, the predicate that a given matrix is such a matrix, embeddability in a fixed dimension, and the basepoint-centered Gram matrix that underlies Schoenberg's characterization.

A configuration of points indexed by ι in k-dimensional Euclidean space is a map x : ι → EuclideanSpace ℝ (Fin k). The squared-distance matrix sqDistMatrix x records dist (x i) (x j) ^ 2. Schoenberg's theorem characterizes which symmetric hollow matrices arise this way through their basepoint-centered Gram matrix.

Main definitions

• DistanceGeometry.sqDistMatrix x : the squared-distance matrix of x.
• DistanceGeometry.IsSqDistMatrix D x : D is the squared-distance matrix of x.
• DistanceGeometry.EmbedsIn D k : D embeds as a squared-distance matrix in EuclideanSpace ℝ (Fin k).
• DistanceGeometry.IsPreDistMatrix D : the project's symmetric-and-hollow structural predicate.
• DistanceGeometry.centeredGram D : the Gram matrix anchored at the base index 0.

Implementation notes

centeredGram uses the fixed base index 0 : Fin n (hence [NeZero n]) as its origin. For a symmetric hollow matrix, changing the base index gives a congruent Gram matrix with the same rank and positive-semidefiniteness. The Schoenberg conditions are therefore basepoint-independent. The point index is Fin n because the base-0 choice uses the order on Fin n; the squared-distance machinery itself only needs Fintype and DecidableEq.

References

• J. von Neumann and I. J. Schoenberg, Fourier integrals and metric geometry, 1941.
• I. J. Schoenberg, Remarks to Maurice Fréchet's article ..., 1935.

noncomputable def DistanceGeometry.sqDistMatrix {n k : ℕ} (x : Fin n → EuclideanSpace ℝ (Fin k)) : Matrix (Fin n) (Fin n) ℝ

The squared-distance matrix of a configuration x: its (i, j) entry is the squared Euclidean distance between x i and x j.

Equations

• DistanceGeometry.sqDistMatrix x = Matrix.of fun (i j : Fin n) => dist (x i) (x j) ^ 2

@[simp]

theorem DistanceGeometry.sqDistMatrix_apply {n k : ℕ} (x : Fin n → EuclideanSpace ℝ (Fin k)) (i j : Fin n) : sqDistMatrix x i j = dist (x i) (x j) ^ 2

def DistanceGeometry.IsSqDistMatrix {n k : ℕ} (D : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → EuclideanSpace ℝ (Fin k)) : Prop

D is the squared-distance matrix of the configuration x when every entry D i j equals the squared Euclidean distance between points x i and x j.

Equations

• DistanceGeometry.IsSqDistMatrix D x = ∀ (i j : Fin n), D i j = dist (x i) (x j) ^ 2

theorem DistanceGeometry.IsSqDistMatrix.eq_sqDistMatrix {n k : ℕ} {D : Matrix (Fin n) (Fin n) ℝ} {x : Fin n → EuclideanSpace ℝ (Fin k)} (hD : IsSqDistMatrix D x) : D = sqDistMatrix x

theorem DistanceGeometry.IsSqDistMatrix.symm {n k : ℕ} {D : Matrix (Fin n) (Fin n) ℝ} {x : Fin n → EuclideanSpace ℝ (Fin k)} (hD : IsSqDistMatrix D x) (i j : Fin n) : D i j = D j i

A squared-distance matrix is symmetric: D i j = D j i.

theorem DistanceGeometry.IsSqDistMatrix.hollow {n k : ℕ} {D : Matrix (Fin n) (Fin n) ℝ} {x : Fin n → EuclideanSpace ℝ (Fin k)} (hD : IsSqDistMatrix D x) (i : Fin n) : D i i = 0

A squared-distance matrix is hollow: its diagonal vanishes.

def DistanceGeometry.EmbedsIn {n : ℕ} (D : Matrix (Fin n) (Fin n) ℝ) (k : ℕ) : Prop

D is embeddable in dimension k when it is the squared-distance matrix of some configuration of points in EuclideanSpace ℝ (Fin k).

Equations

• DistanceGeometry.EmbedsIn D k = ∃ (x : Fin n → EuclideanSpace ℝ (Fin k)), DistanceGeometry.IsSqDistMatrix D x

def DistanceGeometry.IsPreDistMatrix {n : ℕ} (D : Matrix (Fin n) (Fin n) ℝ) : Prop

IsPreDistMatrix is this project's name for the symmetric-and-hollow structural predicate. It does not include entrywise nonnegativity. Every squared-distance matrix satisfies this predicate, which supplies the structural hypothesis for the sufficiency direction of Schoenberg's theorem.

Equations

• DistanceGeometry.IsPreDistMatrix D = ((∀ (i j : Fin n), D i j = D j i) ∧ ∀ (i : Fin n), D i i = 0)

theorem DistanceGeometry.IsPreDistMatrix.symm {n : ℕ} {D : Matrix (Fin n) (Fin n) ℝ} (hD : IsPreDistMatrix D) (i j : Fin n) : D i j = D j i

A matrix satisfying IsPreDistMatrix is symmetric.

theorem DistanceGeometry.IsPreDistMatrix.hollow {n : ℕ} {D : Matrix (Fin n) (Fin n) ℝ} (hD : IsPreDistMatrix D) (i : Fin n) : D i i = 0

A matrix satisfying IsPreDistMatrix is hollow.

theorem DistanceGeometry.IsSqDistMatrix.isPreDistMatrix {n k : ℕ} {D : Matrix (Fin n) (Fin n) ℝ} {x : Fin n → EuclideanSpace ℝ (Fin k)} (hD : IsSqDistMatrix D x) : IsPreDistMatrix D

Every squared-distance matrix satisfies IsPreDistMatrix.

noncomputable def DistanceGeometry.centeredGram {n : ℕ} [NeZero n] (D : Matrix (Fin n) (Fin n) ℝ) : Matrix (Fin n) (Fin n) ℝ

The basepoint-centered Gram matrix of a squared-distance matrix D, anchored at index 0 (requires n ≥ 1, i.e. [NeZero n], for the index 0 : Fin n to exist). When D holds the squared distances of a configuration x, this matrix equals ⟪x i - x 0, x j - x 0⟫ (proved in Schoenberg.lean), hence it is the Gram matrix of the recentred vectors x i - x 0.

Equations

• DistanceGeometry.centeredGram D = Matrix.of fun (i j : Fin n) => (D 0 i + D 0 j - D i j) / 2

@[simp]

theorem DistanceGeometry.centeredGram_apply {n : ℕ} [NeZero n] (D : Matrix (Fin n) (Fin n) ℝ) (i j : Fin n) : centeredGram D i j = (D 0 i + D 0 j - D i j) / 2

theorem DistanceGeometry.centeredGram_symm {n : ℕ} [NeZero n] {D : Matrix (Fin n) (Fin n) ℝ} (hsymm : ∀ (i j : Fin n), D i j = D j i) (i j : Fin n) : centeredGram D i j = centeredGram D j i

The basepoint-centered Gram matrix of a symmetric matrix is symmetric.