V_RS_quartic

formal source

  88/-! ## §2. Quartic-Order Taylor Expansion -/
  89
  90/-- The quartic Taylor approximation to the RS potential about the vacuum. -/
  91def V_RS_quartic (Λ v h : ℝ) : ℝ :=
  92  Λ ^ 4 * ((h / v) ^ 2 / 2 + (h / v) ^ 4 / 24)
  93
  94/-- Mathlib truncation lemma, restated for real `t` to depth 6.
  95
  96    `|exp t − (1 + t + t²/2 + t³/6 + t⁴/24 + t⁵/120)| ≤ exp |t| · |t|⁶`.
  97
  98    Proof: lift to ℂ and apply `Complex.norm_exp_sub_sum_le_norm_mul_exp`. -/
  99private theorem exp_sub_trunc6_le (t : ℝ) :
 100    |Real.exp t - (1 + t + t ^ 2 / 2 + t ^ 3 / 6 + t ^ 4 / 24 + t ^ 5 / 120)| ≤
 101      Real.exp |t| * |t| ^ 6 := by
 102  have h := Complex.norm_exp_sub_sum_le_norm_mul_exp (t : ℂ) 6
 103  have hexpr :
 104      Complex.exp (t : ℂ) - ∑ m ∈ Finset.range 6, (t : ℂ) ^ m / m.factorial =
 105        ((Real.exp t - (1 + t + t ^ 2 / 2 + t ^ 3 / 6 + t ^ 4 / 24 + t ^ 5 / 120) : ℝ) : ℂ) := by
 106    simp [Complex.ofReal_exp, Finset.sum_range_succ, Nat.factorial]
 107  rw [hexpr, Complex.norm_real, Real.norm_eq_abs] at h
 108  simpa [mul_comm, mul_left_comm, mul_assoc] using h
 109
 110/-- Quartic-error bound for `cosh ε - 1` on `|ε| ≤ 1/2`:
 111
 112    `|cosh ε - 1 - ε²/2 - ε⁴/24| ≤ exp |ε| · |ε|⁶`.
 113
 114    Proof: average the truncation bound for `exp t` and `exp (-t)`. -/
 115private theorem cosh_quartic_error (ε : ℝ) :
 116    |Real.cosh ε - 1 - ε ^ 2 / 2 - ε ^ 4 / 24| ≤ Real.exp |ε| * |ε| ^ 6 := by
 117  set P : ℝ → ℝ := fun t =>
 118    1 + t + t ^ 2 / 2 + t ^ 3 / 6 + t ^ 4 / 24 + t ^ 5 / 120
 119  have hpos : |Real.exp ε - P ε| ≤ Real.exp |ε| * |ε| ^ 6 := by
 120    simpa [P] using exp_sub_trunc6_le ε
 121  have hneg : |Real.exp (-ε) - P (-ε)| ≤ Real.exp |ε| * |ε| ^ 6 := by