FlatSimplicialComplex

formal source

  70/-- A flat-background simplicial complex: finitely many hinges (indexed
  71    by `Fin nH`), finitely many edges (`Fin nE`), each hinge satisfying
  72    the flat-sum condition. -/
  73structure FlatSimplicialComplex (nH nE : ℕ) where
  74  hinges : Fin nH → SimplicialHingeData
  75  edges_length_flat : Fin nE → ℝ
  76  edges_length_pos : ∀ e, 0 < edges_length_flat e
  77  flat_all : ∀ h : Fin nH,
  78    DihedralAngle.FlatSumCondition (hinges h).dihedrals
  79
  80/-- A perturbation of the flat edge-lengths. -/
  81structure EdgePerturbation (nE : ℕ) where
  82  eta : Fin nE → ℝ
  83
  84/-- Linearization coefficients: for each (hinge, edge) pair, the partial
  85    derivative of the deficit angle with respect to the edge length,
  86    evaluated at the flat background. -/
  87structure LinearizationCoefficients (nH nE : ℕ) extends
  88    DeficitDerivativeMatrix nH nE
  89
  90/-! ## §2. Predicted deficit
  91
  92Given linearization coefficients, the predicted deficit at each hinge
  93under perturbation `η` is
  94
  95  `δ̂_h = - Σ_e (∂θ_h / ∂L_e) · η_e`
  96
  97(the minus sign because deficit = 2π − totalTheta). -/
  98
  99/-- Linearized deficit at hinge `h` under perturbation `η`. -/
 100def linearizedDeficit {nH nE : ℕ}
 101    (M : LinearizationCoefficients nH nE) (η : EdgePerturbation nE)
 102    (h : Fin nH) : ℝ :=
 103  - (∑ e : Fin nE, M.dThetadL h e * η.eta e)