cosh_quartic_error

formal source

 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
 122    simpa [P, abs_neg] using exp_sub_trunc6_le (-ε)
 123  have hpoly : P ε + P (-ε) = 2 * (1 + ε ^ 2 / 2 + ε ^ 4 / 24) := by
 124    simp only [P]; ring
 125  have hrewrite :
 126      Real.cosh ε - 1 - ε ^ 2 / 2 - ε ^ 4 / 24 =
 127        ((Real.exp ε - P ε) + (Real.exp (-ε) - P (-ε))) / 2 := by
 128    rw [Real.cosh_eq]
 129    linarith [hpoly]
 130  rw [hrewrite, abs_div, abs_of_pos (by norm_num : (0 : ℝ) < 2)]
 131  calc
 132    |(Real.exp ε - P ε) + (Real.exp (-ε) - P (-ε))| / 2
 133        ≤ (|Real.exp ε - P ε| + |Real.exp (-ε) - P (-ε)|) / 2 :=
 134          div_le_div_of_nonneg_right (abs_add_le _ _) (by norm_num)
 135    _ ≤ (Real.exp |ε| * |ε| ^ 6 + Real.exp |ε| * |ε| ^ 6) / 2 :=
 136          div_le_div_of_nonneg_right (add_le_add hpos hneg) (by norm_num)
 137    _ = Real.exp |ε| * |ε| ^ 6 := by ring
 138
 139/-- Quartic Taylor identity for `J(exp ε)` at depth 4:
 140
 141    `|J(exp ε) - ε²/2 - ε⁴/24| ≤ exp |ε| · |ε|⁶`. -/
 142theorem jcost_quartic_error (ε : ℝ) :
 143    |Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24| ≤ Real.exp |ε| * |ε| ^ 6 := by
 144  have h := cosh_quartic_error ε
 145  have hcosh : Jcost (Real.exp ε) = Real.cosh ε - 1 := Cost.Jcost_exp_cosh ε