exact_decomposition

formal source

 207    not just small `ε`. In the weak-field regime the remainder is
 208    `O(|ε|⁴)` and negligible; in the strong-field regime it is
 209    the physical content of the non-linear coupling. -/
 210theorem exact_decomposition {n : ℕ} (G : WeightedLedgerGraph n)
 211    (ε : LogPotential n) :
 212    exactJCostAction G ε = laplacian_action G ε + quarticRemainder G ε := by
 213  rw [laplacian_action_prod_form]
 214  unfold exactJCostAction quarticRemainder coshRemainder
 215  -- Right side: (1/2) Σ Σ w x² + Σ Σ w (cosh - 1 - x²/2)
 216  --         = Σ Σ w [x²/2 + cosh - 1 - x²/2]
 217  --         = Σ Σ w (cosh - 1) = left side.
 218  rw [show (1 : ℝ) / 2 * ∑ i : Fin n, ∑ j : Fin n, G.weight i j * (ε i - ε j) ^ 2
 219        = ∑ i : Fin n, ∑ j : Fin n, G.weight i j * ((ε i - ε j) ^ 2 / 2) by
 220      rw [Finset.mul_sum]
 221      apply Finset.sum_congr rfl
 222      intro i _
 223      rw [Finset.mul_sum]
 224      apply Finset.sum_congr rfl
 225      intro j _
 226      ring]
 227  rw [← Finset.sum_add_distrib]
 228  apply Finset.sum_congr rfl
 229  intro i _
 230  rw [← Finset.sum_add_distrib]
 231  apply Finset.sum_congr rfl
 232  intro j _
 233  ring
 234
 235/-- **WEAK-FIELD LIMIT.** When every log-potential difference is
 236    zero, `exactJCostAction = laplacian_action = 0`. This is the
 237    flat vacuum limit. -/
 238theorem exact_flat_agrees_with_linearized {n : ℕ}
 239    (G : WeightedLedgerGraph n) :
 240    exactJCostAction G (fun _ => (0 : ℝ))