edgeSqFirstOrder

formal source

 136    Second order: `δ²(ℓ²/ℓ_0²) = (ξ_i + ξ_j)² / 2`.
 137
 138    These are the building blocks for §3. -/
 139def edgeSqFirstOrder {n : ℕ} (ε : LogPotential n) (i j : Fin n) : ℝ :=
 140  ε i + ε j
 141
 142def edgeSqSecondOrder {n : ℕ} (ε : LogPotential n) (i j : Fin n) : ℝ :=
 143  (ε i + ε j) ^ 2 / 2
 144
 145/-- The conformal expansion writes `ℓ²/ℓ_0² − 1 − δ¹ − δ²` as the
 146    remainder. This is a tautology after `conformal_length_sq_taylor2`
 147    but it is the form that downstream "second-order action" reductions
 148    need. -/
 149theorem conformal_length_sq_decomposition
 150    {n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n) (i j : Fin n) :
 151    (conformal_edge_length_field a ha ε).length i j ^ 2 / a ^ 2
 152      = 1 + edgeSqFirstOrder ε i j + edgeSqSecondOrder ε i j
 153        + conformal_remainder (ε i + ε j) := by
 154  unfold edgeSqFirstOrder edgeSqSecondOrder
 155  exact conformal_length_sq_taylor2 a ha ε i j
 156
 157/-! ## §2. Graph-Laplacian decomposition
 158
 159The pure-algebraic identity that drives the reduction. If `M_{ij}` is
 160symmetric with zero row sums, then `ξ ↦ Σ_{i,j} M_{ij} ξ_i ξ_j` is the
 161discrete Dirichlet energy `−½ Σ_{i,j} M_{ij} (ξ_i − ξ_j)²`.
 162
 163This is the discrete analog of `∫ φ Δφ = −∫ |∇φ|²` (integration by parts
 164on a closed manifold) and is what makes a "Regge bilinear form on edges"
 165manifestly the same as a "Dirichlet form on vertices". -/
 166
 167/-- The Dirichlet form generated by a symmetric matrix `M` and a vertex
 168    function `ξ`: `D[ξ; M] = ½ Σ_{i,j} M_{ij} (ξ_i − ξ_j)²`. -/
 169def dirichletForm {n : ℕ} (M : Fin n → Fin n → ℝ) (ε : LogPotential n) : ℝ :=