cosh_quartic_error

proof body

Tactic-mode proof.

 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 |ε| · |ε|⁶`. -/