arctan_le_upper_poly
Arctan x is bounded above by the polynomial x minus x cubed over three plus x to the fifth over five for every nonnegative real x. Numerics workers in Recognition Science cite the result when building constructive interval enclosures for arctangent. The argument reduces the claim to nonnegativity of the difference function on the ray from zero, then applies monotoneOn_of_deriv_nonneg after verifying the derivative stays nonnegative via the comparison 1 minus t squared plus t to the fourth is at least one over one plus t squared.
claimFor every real number $x$ with $x$ nonnegative, $arctan x$ is at most $x - x^3/3 + x^5/5$.
background
The module Numerics.Interval.Trig supplies rigorous interval bounds for arctan and tan. The upper bounding polynomial g_upper is defined by g_upper(x) = x - x^3/3 + x^5/5. Its derivative equals 1 - t^2 + t^4, which the module compares against the derivative of arctan, namely 1/(1 + t^2). The comparison rests on the auxiliary result inv_one_add_sq_le_upper, which asserts that 1 - t^2 + t^4 is at least 1/(1 + t^2) for t nonnegative. The module documentation states that both the upper and lower polynomial bounds are antiderivatives of their respective bounding functions and that the comparison follows from monotoneOn_of_deriv_nonneg on the interval from zero to infinity.
proof idea
The proof first reduces the target inequality to nonnegativity of g_upper x minus arctan x. It then applies monotoneOn_of_deriv_nonneg to the difference on the convex set from zero to infinity, using continuity of the difference from g_upper_continuous and continuity of arctan. Differentiability of the difference follows from g_upper_differentiable together with the standard hasDerivAt_arctan. The derivative of the difference is rewritten as (1 - t^2 + t^4) minus 1/(1 + t^2) and shown nonnegative by inv_one_add_sq_le_upper. The value of the difference at zero is zero by direct simplification, so monotonicity yields the bound for arbitrary nonnegative x.
why it matters in Recognition Science
This theorem supplies the upper half of the enclosure for arctan(1/3) inside arctan_one_third_in_interval. That enclosure is required for the identity arctan(2) equals pi over four plus arctan(1/3) and for subsequent constructive bounds on pi in the Recognition Science numerics pipeline. It directly instantiates the derivative-comparison technique described in the module documentation for building interval arithmetic without hidden hypotheses.
scope and limits
- Does not apply for negative x.
- Does not supply a matching lower bound.
- Does not quantify the remainder term.
- Does not address complex arguments.
Lean usage
theorem arctan_one_third_upper : arctan (1/3) ≤ g_upper (1/3) := arctan_le_upper_poly (1/3) (by norm_num)formal statement (Lean)
63theorem arctan_le_upper_poly (x : ℝ) (hx : 0 ≤ x) : arctan x ≤ g_upper x := by
proof body
Term-mode proof.
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 -/