arctan_le_upper_poly

formal source

  60  rw [this]; linarith [sq_nonneg (t ^ 3)]
  61
  62/-- `arctan(x) ≤ x − x³/3 + x⁵/5` for x ≥ 0. -/
  63theorem arctan_le_upper_poly (x : ℝ) (hx : 0 ≤ x) : arctan x ≤ g_upper x := by
  64  suffices h : 0 ≤ g_upper x - arctan x by linarith
  65  have hkey : MonotoneOn (fun t => g_upper t - arctan t) (Set.Ici 0) :=
  66    monotoneOn_of_deriv_nonneg (convex_Ici 0)
  67      ((g_upper_continuous.sub continuous_arctan).continuousOn)
  68      (fun t _ => ((g_upper_differentiable t).sub
  69        (hasDerivAt_arctan t).differentiableAt).differentiableWithinAt)
  70      (fun t ht => by
  71        simp only [Set.nonempty_Iio, interior_Ici'] at ht
  72        have hd : HasDerivAt (fun s => g_upper s - arctan s)
  73          ((1 - t^2 + t^4) - 1/(1+t^2)) t :=
  74          (g_upper_deriv t).sub (hasDerivAt_arctan t)
  75        rw [hd.deriv]
  76        linarith [inv_one_add_sq_le_upper t])
  77  linarith [hkey (Set.mem_Ici.mpr (le_refl 0)) (Set.mem_Ici.mpr hx) hx,
  78            show g_upper 0 - arctan 0 = 0 by simp [g_upper, arctan_zero]]
  79
  80/-- Lower bounding polynomial: h(x) = x − x³/3 + x⁵/5 − x⁷/7 -/
  81private noncomputable def h_lower (x : ℝ) : ℝ := x - x ^ 3 / 3 + x ^ 5 / 5 - x ^ 7 / 7
  82
  83private theorem h_lower_continuous : Continuous h_lower := by unfold h_lower; fun_prop
  84private theorem h_lower_differentiable : Differentiable ℝ h_lower := by unfold h_lower; fun_prop
  85
  86private theorem h_lower_deriv (t : ℝ) :
  87    HasDerivAt h_lower (1 - t ^ 2 + t ^ 4 - t ^ 6) t := by
  88  unfold h_lower
  89  have := (((hasDerivAt_id t).sub ((hasDerivAt_pow 3 t).div_const 3)).add
  90    ((hasDerivAt_pow 5 t).div_const 5)).sub ((hasDerivAt_pow 7 t).div_const 7)
  91  convert this using 1; ring
  92
  93/-- Key inequality: `1 − t² + t⁴ − t⁶ ≤ 1/(1+t²)` for all t.