theorem
proved
tactic proof
regge_sum_cubicHinges
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
208 unfold regge_sum cubicHinges cubicDeficitFunctional
209 simp only
210 -- Reduce `((toList).map singletonHinge).map (fun h => area*deficit) |>.sum`
211 rw [List.map_map]
212 have h_point : ∀ ij : Fin n × Fin n,
213 ((fun h => cubicArea (conformal_edge_length_field a ha ε) h *
214 cubicDeficit (conformal_edge_length_field a ha ε) h) ∘
215 (fun ij' => singletonHinge ij'.1 ij'.2 (G.weight ij'.1 ij'.2)
216 (G.weight_nonneg ij'.1 ij'.2))) ij
217 = (jcost_to_regge_factor / 2) * G.weight ij.1 ij.2 *
218 (ε ij.1 - ε ij.2) ^ 2 := by
219 intro ij
220 simp only [Function.comp_apply]
221 exact singletonHinge_product a ha ε ij.1 ij.2 _ _
222 -- Convert the `toList.map` sum to a Finset.sum using `List.sum_toFinset`
223 -- and `Finset.toList_toFinset`.
224 have h_sum :
225 (((Finset.univ : Finset (Fin n × Fin n)).toList.map
226 (fun ij => (jcost_to_regge_factor / 2) * G.weight ij.1 ij.2 *
227 (ε ij.1 - ε ij.2) ^ 2))).sum
228 = ∑ ij : Fin n × Fin n,
229 (jcost_to_regge_factor / 2) * G.weight ij.1 ij.2 * (ε ij.1 - ε ij.2) ^ 2 := by
230 rw [← List.sum_toFinset _ (Finset.nodup_toList _)]
231 rw [Finset.toList_toFinset]
232 calc
233 ((Finset.univ : Finset (Fin n × Fin n)).toList.map
234 ((fun h => cubicArea (conformal_edge_length_field a ha ε) h *
235 cubicDeficit (conformal_edge_length_field a ha ε) h) ∘
236 (fun ij => singletonHinge ij.1 ij.2 (G.weight ij.1 ij.2)
237 (G.weight_nonneg ij.1 ij.2)))).sum
238 = ((Finset.univ : Finset (Fin n × Fin n)).toList.map
239 (fun ij => (jcost_to_regge_factor / 2) * G.weight ij.1 ij.2 *
240 (ε ij.1 - ε ij.2) ^ 2)).sum := by
241 congr 1
242 apply List.map_congr_left
243 intro ij _
244 exact h_point ij
245 _ = ∑ ij : Fin n × Fin n,
246 (jcost_to_regge_factor / 2) * G.weight ij.1 ij.2 *
247 (ε ij.1 - ε ij.2) ^ 2 := h_sum
248 _ = (jcost_to_regge_factor / 2) *
249 (∑ ij : Fin n × Fin n, G.weight ij.1 ij.2 * (ε ij.1 - ε ij.2) ^ 2) := by
250 rw [Finset.mul_sum]
251 apply Finset.sum_congr rfl
252 intro ij _
253 ring
254
255/-! ## §7. Matching the Laplacian action -/
256
257/-- The Laplacian action as a single Finset sum over `Fin n × Fin n`. -/