singletonHinge_product

formal source

 176
 177/-- Area × deficit at a singleton hinge for pair `(i, j)`, on the
 178    conformal edge-length field. -/
 179theorem singletonHinge_product {n : ℕ} (a : ℝ) (ha : 0 < a)
 180    (ε : LogPotential n) (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
 181    cubicArea (conformal_edge_length_field a ha ε) (singletonHinge i j w hw) *
 182      cubicDeficit (conformal_edge_length_field a ha ε) (singletonHinge i j w hw)
 183    = (jcost_to_regge_factor / 2) * w * (ε i - ε j) ^ 2 := by
 184  rw [cubicArea_singleton, cubicDeficit_singleton,
 185      recoverEps_conformal a ha ε i, recoverEps_conformal a ha ε j]
 186  ring
 187
 188/-! ## §5. The cubic hinge list via `Finset.univ.toList`
 189
 190Enumerate one hinge per ordered pair `(i, j) ∈ Fin n × Fin n`. Pairs with
 191`i = j` contribute 0 because `(ε_i − ε_i)² = 0`. -/
 192
 193/-- The hinge list: one singleton hinge per ordered pair. -/
 194def cubicHinges {n : ℕ} (G : WeightedLedgerGraph n) : List (HingeDatum n) :=
 195  (Finset.univ : Finset (Fin n × Fin n)).toList.map (fun ij =>
 196    singletonHinge ij.1 ij.2 (G.weight ij.1 ij.2) (G.weight_nonneg ij.1 ij.2))
 197
 198/-! ## §6. Summing the hinge list — reduction to a `Finset.sum` -/
 199
 200/-- The Regge sum on `cubicHinges G` equals `(κ/2)` times the Finset
 201    sum over `Fin n × Fin n` of `G.weight i j · (ε_i − ε_j)²`. -/
 202theorem regge_sum_cubicHinges {n : ℕ} (a : ℝ) (ha : 0 < a)
 203    (ε : LogPotential n) (G : WeightedLedgerGraph n) :
 204    regge_sum (cubicDeficitFunctional n) (conformal_edge_length_field a ha ε)
 205        (cubicHinges G)
 206    = (jcost_to_regge_factor / 2) *
 207        (∑ ij : Fin n × Fin n, G.weight ij.1 ij.2 * (ε ij.1 - ε ij.2) ^ 2) := by
 208  unfold regge_sum cubicHinges cubicDeficitFunctional
 209  simp only