coshRemainder_zero

formal source

 165  linarith
 166
 167/-- The cosh remainder is zero at `x = 0` (the flat vacuum). -/
 168theorem coshRemainder_zero : coshRemainder 0 = 0 := by
 169  unfold coshRemainder
 170  simp
 171
 172/-! ## §4. Decomposition: exact = linearized + quartic remainder -/
 173
 174/-- The quartic remainder of the full action (the "non-linear
 175    correction" to the weak-field Laplacian). It vanishes on the
 176    flat vacuum and is `O(|ε|⁴)` for small `ε`. -/
 177def quarticRemainder {n : ℕ} (G : WeightedLedgerGraph n)
 178    (ε : LogPotential n) : ℝ :=
 179  ∑ i : Fin n, ∑ j : Fin n,
 180    G.weight i j * coshRemainder (ε i - ε j)
 181
 182/-- The quartic remainder is non-negative. -/
 183theorem quarticRemainder_nonneg {n : ℕ} (G : WeightedLedgerGraph n)
 184    (ε : LogPotential n) : 0 ≤ quarticRemainder G ε := by
 185  unfold quarticRemainder
 186  apply Finset.sum_nonneg
 187  intro i _
 188  apply Finset.sum_nonneg
 189  intro j _
 190  exact mul_nonneg (G.weight_nonneg i j) (coshRemainder_nonneg _)
 191
 192/-- Helper: the laplacian action as the product-sum of quadratic terms. -/
 193private theorem laplacian_action_prod_form {n : ℕ}
 194    (G : WeightedLedgerGraph n) (ε : LogPotential n) :
 195    laplacian_action G ε
 196      = (1 / 2) * ∑ i : Fin n, ∑ j : Fin n,
 197          G.weight i j * (ε i - ε j) ^ 2 := by
 198  unfold laplacian_action