conformal_remainder

formal source

 109    remainder. We do *not* prove a quantitative bound here (Mathlib's
 110    `Real.exp_taylor_lt` route is heavy); we just expose the algebraic
 111    decomposition with the remainder named explicitly. -/
 112def conformal_remainder (t : ℝ) : ℝ := Real.exp t - 1 - t - t ^ 2 / 2
 113
 114/-- The second-order conformal expansion. This is *exact* with the
 115    remainder explicitly named: it is just the rearrangement of
 116    `exp(t) = 1 + t + t²/2 + R(t)`. -/
 117theorem conformal_length_sq_taylor2
 118    {n : ℕ} (a : ℝ) (ha : 0 < a) (ε : LogPotential n) (i j : Fin n) :
 119    (conformal_edge_length_field a ha ε).length i j ^ 2 / a ^ 2
 120      = 1 + (ε i + ε j) + (ε i + ε j) ^ 2 / 2
 121        + conformal_remainder (ε i + ε j) := by
 122  have ha2 : (a : ℝ) ^ 2 ≠ 0 := pow_ne_zero 2 (ne_of_gt ha)
 123  rw [conformal_length_sq_exact a ha ε i j]
 124  unfold conformal_remainder
 125  field_simp
 126  ring
 127
 128/-- At the flat vacuum `ξ ≡ 0`, the conformal remainder vanishes. -/
 129theorem conformal_remainder_zero : conformal_remainder 0 = 0 := by
 130  unfold conformal_remainder
 131  simp
 132
 133/-- The first- and second-order coefficients of `ℓ_{ij}² / ℓ_0²` in `ξ`.
 134
 135    First order:  `δ¹(ℓ²/ℓ_0²) = ξ_i + ξ_j`.
 136    Second order: `δ²(ℓ²/ℓ_0²) = (ξ_i + ξ_j)² / 2`.
 137
 138    These are the building blocks for §3. -/
 139def edgeSqFirstOrder {n : ℕ} (ε : LogPotential n) (i j : Fin n) : ℝ :=
 140  ε i + ε j
 141
 142def edgeSqSecondOrder {n : ℕ} (ε : LogPotential n) (i j : Fin n) : ℝ :=