pith. machine review for the scientific record. sign in
structure definition def or abbrev

as

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)

 130structure as the Laplacian action. The identification is:
 131
 132  (1/2) Σ_{i~j} w_ij · (ε_i − ε_j)² = (1/κ) Σ_h δ_h · A_h
 133
 134with w_ij = A_ij / (κ · vol_i) where A_ij is the shared face area
 135and vol_i is the simplex volume. -/
 136
 137/-- The Regge action density at a hinge. -/

used by (40)

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

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.