h_lower_differentiable

formal source

  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.
  94    Proof: `(1−t²+t⁴−t⁶)(1+t²) = 1−t⁸ ≤ 1`. -/
  95private theorem lower_le_inv_one_add_sq (t : ℝ) :
  96    1 - t ^ 2 + t ^ 4 - t ^ 6 ≤ 1 / (1 + t ^ 2) := by
  97  rw [le_div_iff₀ (by positivity : 0 < 1 + t ^ 2)]
  98  have : (1 - t ^ 2 + t ^ 4 - t ^ 6) * (1 + t ^ 2) = 1 - t ^ 8 := by ring
  99  rw [this]; linarith [sq_nonneg (t ^ 4)]
 100
 101/-- `x − x³/3 + x⁵/5 − x⁷/7 ≤ arctan(x)` for x ≥ 0. -/
 102theorem lower_poly_le_arctan (x : ℝ) (hx : 0 ≤ x) : h_lower x ≤ arctan x := by
 103  suffices h : 0 ≤ arctan x - h_lower x by linarith
 104  have hkey : MonotoneOn (fun t => arctan t - h_lower t) (Set.Ici 0) :=
 105    monotoneOn_of_deriv_nonneg (convex_Ici 0)
 106      ((continuous_arctan.sub h_lower_continuous).continuousOn)
 107      (fun t _ => ((hasDerivAt_arctan t).differentiableAt.sub
 108        (h_lower_differentiable t)).differentiableWithinAt)
 109      (fun t ht => by
 110        simp only [Set.nonempty_Iio, interior_Ici'] at ht
 111        have hd : HasDerivAt (fun s => arctan s - h_lower s)
 112          (1/(1+t^2) - (1 - t^2 + t^4 - t^6)) t :=
 113          (hasDerivAt_arctan t).sub (h_lower_deriv t)
 114        rw [hd.deriv]