IndisputableMonolith.Geometry.CayleyMengerN

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Data.Matrix.Basic
   3import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
   4
   5/-!
   6# Dimension-Parametric Cayley-Menger Matrix
   7
   8This module starts the n-dimensional generalization after the 3D
   9tetrahedral closure: instead of expanding the determinant as a polynomial,
  10we define the full Cayley-Menger matrix for an arbitrary `n`-simplex using
  11Mathlib matrices and determinants.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Geometry
  16namespace CayleyMengerN
  17
  18noncomputable section
  19
  20/-- Squared-distance data for an `n`-simplex with vertices `Fin (n+1)`. -/
  21structure SimplexSquaredDistances (n : ℕ) where
  22  distSq : Fin (n + 1) → Fin (n + 1) → ℝ
  23  symm : ∀ i j, distSq i j = distSq j i
  24  diag_zero : ∀ i, distSq i i = 0
  25
  26/-- Convert a Cayley-Menger matrix index to an optional simplex vertex.
  27Index `0` is the leading Cayley-Menger row/column; index `k+1` represents
  28simplex vertex `k`. -/
  29def cmIndexVertex {n : ℕ} (i : Fin (n + 2)) : Option (Fin (n + 1)) :=
  30  if h : i.val = 0 then none
  31  else some ⟨i.val - 1, by omega⟩
  32
  33/-- The full `(n+2) × (n+2)` Cayley-Menger matrix. -/
  34def cmMatrixN {n : ℕ} (D : SimplexSquaredDistances n) :
  35    Matrix (Fin (n + 2)) (Fin (n + 2)) ℝ :=
  36  fun i j =>
  37    match cmIndexVertex i, cmIndexVertex j with
  38    | none, none => 0
  39    | none, some _ => 1
  40    | some _, none => 1
  41    | some vi, some vj => D.distSq vi vj
  42
  43/-- The n-dimensional Cayley-Menger determinant. -/
  44def cmDetN {n : ℕ} (D : SimplexSquaredDistances n) : ℝ :=
  45  Matrix.det (cmMatrixN D)
  46
  47/-- The formal squared-volume expression:
  48
  49`V_n^2 = (-1)^(n+1) det(CM) / (2^n (n!)^2)`.
  50-/
  51def simplexVolumeSqN {n : ℕ} (D : SimplexSquaredDistances n) : ℝ :=
  52  ((-1 : ℝ) ^ (n + 1) * cmDetN D) /
  53    ((2 : ℝ) ^ n * ((Nat.factorial n : ℕ) : ℝ) ^ 2)
  54
  55/-- The Cayley-Menger matrix is symmetric whenever the squared-distance
  56data is symmetric. -/
  57theorem cmMatrixN_symm {n : ℕ} (D : SimplexSquaredDistances n)
  58    (i j : Fin (n + 2)) :
  59    cmMatrixN D i j = cmMatrixN D j i := by
  60  unfold cmMatrixN
  61  cases cmIndexVertex i <;> cases cmIndexVertex j <;> simp
  62  exact D.symm _ _
  63
  64end
  65
  66end CayleyMengerN
  67end Geometry
  68end IndisputableMonolith
  69