coshRemainder

formal source

 155    weak-field limit of `exactJCostAction`. The remainder is the
 156    "non-linear cosh correction":
 157    `cosh(x) − 1 − x²/2 = x⁴/24 + O(x⁶)`. -/
 158def coshRemainder (x : ℝ) : ℝ := Real.cosh x - 1 - x ^ 2 / 2
 159
 160/-- The cosh remainder is non-negative for all `x` (because
 161    `cosh x ≥ 1 + x²/2` — a Taylor lower bound). -/
 162theorem coshRemainder_nonneg (x : ℝ) : 0 ≤ coshRemainder x := by
 163  unfold coshRemainder
 164  have h := cosh_quadratic_lower_bound x
 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