quadraticForm

formal source

 170  (1 / 2) * ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2
 171
 172/-- The bilinear form: `Q[ξ; M] = Σ_{i,j} M_{ij} ξ_i ξ_j`. -/
 173def quadraticForm {n : ℕ} (M : Fin n → Fin n → ℝ) (ε : LogPotential n) : ℝ :=
 174  ∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j
 175
 176/-- Helper: pulling a constant out of a sum (right-multiplication form). -/
 177private lemma sum_const_mul_right {n : ℕ} (f : Fin n → ℝ) (c : ℝ) :
 178    ∑ j : Fin n, f j * c = (∑ j : Fin n, f j) * c := by
 179  rw [← Finset.sum_mul]
 180
 181/-- Helper: pulling a constant out of an inner sum at `j` (when the inner
 182    factor depends only on `i`). -/
 183private lemma inner_sum_const {n : ℕ} (M : Fin n → Fin n → ℝ) (g : Fin n → ℝ) (i : Fin n) :
 184    ∑ j : Fin n, M i j * g i = (∑ j : Fin n, M i j) * g i :=
 185  sum_const_mul_right (fun j => M i j) (g i)
 186
 187/-- **GRAPH-LAPLACIAN DECOMPOSITION.**
 188    For symmetric `M` with zero row sums,
 189    `Q[ξ; M] = −D[ξ; M]`.
 190
 191    This is the algebraic core of the weak-field reduction. -/
 192theorem dirichlet_eq_neg_quadratic
 193    {n : ℕ} (M : Fin n → Fin n → ℝ)
 194    (hsymm : ∀ i j, M i j = M j i)
 195    (hrow : ∀ i, ∑ j : Fin n, M i j = 0)
 196    (ε : LogPotential n) :
 197    quadraticForm M ε = - dirichletForm M ε := by
 198  unfold quadraticForm dirichletForm
 199  -- Expand `(ε i − ε j)² = ε i² − 2 ε i ε j + ε j²` and sum.
 200  have hkey : ∀ i j, M i j * (ε i - ε j) ^ 2
 201              = M i j * (ε i) ^ 2 - 2 * (M i j * ε i * ε j)
 202                + M i j * (ε j) ^ 2 := by
 203    intro i j; ring