pith. machine review for the scientific record. sign in
theorem proved term proof

laplacian_action_as_prod_sum

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 258theorem laplacian_action_as_prod_sum {n : ℕ}
 259    (G : WeightedLedgerGraph n) (ε : LogPotential n) :
 260    laplacian_action G ε
 261    = (1 / 2) *
 262        (∑ ij : Fin n × Fin n, G.weight ij.1 ij.2 * (ε ij.1 - ε ij.2) ^ 2) := by

proof body

Term-mode proof.

 263  unfold laplacian_action
 264  congr 1
 265  rw [show (Finset.univ : Finset (Fin n × Fin n)) =
 266      (Finset.univ : Finset (Fin n)) ×ˢ (Finset.univ : Finset (Fin n))
 267      from (Finset.univ_product_univ).symm]
 268  exact (Finset.sum_product' (s := (Finset.univ : Finset (Fin n)))
 269      (t := (Finset.univ : Finset (Fin n)))
 270      (f := fun i j => G.weight i j * (ε i - ε j) ^ 2)).symm
 271
 272/-! ## §8. The cubic linearization discharge -/
 273
 274/-- **MAIN THEOREM.** The `ReggeDeficitLinearizationHypothesis` is
 275    discharged unconditionally for any weighted ledger graph `G` using
 276    the cubic deficit functional and hinge list. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.