IndisputableMonolith.Geometry.SchlaefliTriangulation3D

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Algebra.BigOperators.Group.Finset.Basic
   3import IndisputableMonolith.Geometry.SchlaefliTetrahedron
   4import IndisputableMonolith.Geometry.ReggeTriangulation3D
   5
   6/-!
   7# Schläfli Identity for Finite 3D Triangulations
   8
   9The global 3D Schläfli cancellation is the finite sum of the local
  10tetrahedral Schläfli identities over top-dimensional simplices.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Geometry
  15namespace SchlaefliTriangulation3D
  16
  17open ReggeTriangulation3D SchlaefliTetrahedron
  18
  19noncomputable section
  20
  21/-- Local Schläfli derivative data on every tetrahedron of a finite
  22triangulation. -/
  23structure TriangulationSchlaefliData (K : Triangulation3D) where
  24  tetData : ∀ τ : Fin K.nT, TetraSchlaefliDerivativeData (K.tet τ)
  25
  26/-- The global Schläfli left-hand side, summed over tetrahedra and local
  27tetrahedral edges. -/
  28def globalSchlaefliLHS (K : Triangulation3D)
  29    (D : TriangulationSchlaefliData K) (e' : Fin 6) : ℝ :=
  30  ∑ τ : Fin K.nT,
  31    ∑ e : Fin 6,
  32      Real.sqrt ((K.tet τ).sqEdge e) * (D.tetData τ).dihedralDeriv e e'
  33
  34/-- The global Schläfli right-hand side: the Euclidean angle-variation term
  35vanishes. -/
  36def globalSchlaefliRHS (K : Triangulation3D)
  37    (_D : TriangulationSchlaefliData K) (_e' : Fin 6) : ℝ :=
  38  0
  39
  40/-- Summing local tetrahedral Schläfli identities gives the global finite
  41triangulation identity. -/
  42theorem global_schlaefli_of_local
  43    (K : Triangulation3D) (D : TriangulationSchlaefliData K) (e' : Fin 6) :
  44    globalSchlaefliLHS K D e' = globalSchlaefliRHS K D e' := by
  45  unfold globalSchlaefliLHS globalSchlaefliRHS
  46  have hlocal : ∀ τ : Fin K.nT,
  47      (∑ e : Fin 6,
  48        Real.sqrt ((K.tet τ).sqEdge e) * (D.tetData τ).dihedralDeriv e e')
  49        = 0 := by
  50    intro τ
  51    exact (D.tetData τ).schlaefli e'
  52  simp_rw [hlocal]
  53  simp
  54
  55end
  56
  57end SchlaefliTriangulation3D
  58end Geometry
  59end IndisputableMonolith
  60