inner_sum_const

formal source

 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
 204  -- Sum the identity term-by-term.
 205  have hsum : ∑ i : Fin n, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2
 206              = (∑ i : Fin n, ∑ j : Fin n, M i j * (ε i) ^ 2)
 207                - 2 * (∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j)
 208                + (∑ i : Fin n, ∑ j : Fin n, M i j * (ε j) ^ 2) := by
 209    have h1 : ∀ i, ∑ j : Fin n, M i j * (ε i - ε j) ^ 2
 210              = ∑ j : Fin n, (M i j * (ε i) ^ 2 - 2 * (M i j * ε i * ε j)
 211                              + M i j * (ε j) ^ 2) := by
 212      intro i; exact Finset.sum_congr rfl (fun j _ => hkey i j)
 213    simp only [h1, Finset.sum_add_distrib, Finset.sum_sub_distrib]