pith. machine review for the scientific record. sign in
theorem proved term proof

exact_decomposition

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)

 210theorem exact_decomposition {n : ℕ} (G : WeightedLedgerGraph n)
 211    (ε : LogPotential n) :
 212    exactJCostAction G ε = laplacian_action G ε + quarticRemainder G ε := by

proof body

Term-mode proof.

 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. -/

used by (2)

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

depends on (16)

Lean names referenced from this declaration's body.