g_upper_continuous

formal source

  41/-- Upper bounding polynomial: g(x) = x − x³/3 + x⁵/5 -/
  42private noncomputable def g_upper (x : ℝ) : ℝ := x - x ^ 3 / 3 + x ^ 5 / 5
  43
  44private theorem g_upper_continuous : Continuous g_upper := by unfold g_upper; fun_prop
  45private theorem g_upper_differentiable : Differentiable ℝ g_upper := by unfold g_upper; fun_prop
  46
  47private theorem g_upper_deriv (t : ℝ) :
  48    HasDerivAt g_upper (1 - t ^ 2 + t ^ 4) t := by
  49  unfold g_upper
  50  have := ((hasDerivAt_id t).sub ((hasDerivAt_pow 3 t).div_const 3)).add
  51    ((hasDerivAt_pow 5 t).div_const 5)
  52  convert this using 1; ring
  53
  54/-- Key inequality: `1/(1+t²) ≤ 1 − t² + t⁴` for all t.
  55    Proof: `(1−t²+t⁴)(1+t²) = 1+t⁶ ≥ 1`. -/
  56private theorem inv_one_add_sq_le_upper (t : ℝ) :
  57    1 / (1 + t ^ 2) ≤ 1 - t ^ 2 + t ^ 4 := by
  58  rw [div_le_iff₀ (by positivity : 0 < 1 + t ^ 2)]
  59  have : (1 - t ^ 2 + t ^ 4) * (1 + t ^ 2) = 1 + t ^ 6 := by ring
  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)