V_RS_quartic_error

formal source

 153
 154/-- The error in approximating `V_RS` by its quartic Taylor polynomial is
 155    bounded uniformly on `|h| ≤ v / 2`. -/
 156theorem V_RS_quartic_error (Λ v h : ℝ) (hv : 0 < v) (hbound : |h| ≤ v / 2) :
 157    |V_RS Λ v h - V_RS_quartic Λ v h|
 158      ≤ |Λ| ^ 4 * (Real.exp |h / v| * |h / v| ^ 6) := by
 159  have hε : |h / v| ≤ 1 / 2 := by
 160    rw [abs_div, abs_of_pos hv]
 161    rw [div_le_iff₀ hv]
 162    linarith
 163  have hcore := jcost_quartic_error (h / v)
 164  -- |V_RS − V_RS_quartic| = |Λ|^4 · |J(exp ε) − ε²/2 − ε⁴/24|
 165  unfold V_RS V_RS_quartic
 166  set ε := h / v
 167  have hL : Λ ^ 4 * Jcost (Real.exp ε) - Λ ^ 4 * (ε ^ 2 / 2 + ε ^ 4 / 24)
 168            = Λ ^ 4 * (Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24) := by ring
 169  rw [hL, abs_mul]
 170  have hΛ : |Λ ^ 4| = |Λ| ^ 4 := by rw [abs_pow]
 171  rw [hΛ]
 172  have hΛ4 : 0 ≤ |Λ| ^ 4 := by positivity
 173  exact mul_le_mul_of_nonneg_left hcore hΛ4
 174
 175/-- The leading quadratic coefficient is forced: `Λ⁴ / (2 v²)`. -/
 176def quadratic_coefficient (Λ v : ℝ) : ℝ := Λ ^ 4 / (2 * v ^ 2)
 177
 178/-- The leading quartic coefficient is forced: `Λ⁴ / (24 v⁴)`. -/
 179def quartic_coefficient_canonical (Λ v : ℝ) : ℝ := Λ ^ 4 / (24 * v ^ 4)
 180
 181/-- Algebraic identity: the quartic Taylor potential equals the canonical
 182    quadratic-plus-quartic Lagrangian potential up to renaming. -/
 183theorem V_RS_quartic_canonical (Λ v : ℝ) (hv : v ≠ 0) (h : ℝ) :
 184    V_RS_quartic Λ v h
 185      = quadratic_coefficient Λ v * h ^ 2
 186        + quartic_coefficient_canonical Λ v * h ^ 4 := by