g_upper
g_upper supplies the explicit polynomial x - x³/3 + x⁵/5 that upper-bounds arctan on [0, ∞) inside the interval-arithmetic module. Numerics researchers constructing certified enclosures for arctan(1/3) and the arctan(2) identity cite this definition when tightening bounds on π. The declaration is a direct polynomial expression whose derivative equals the rational function 1 - t² + t⁴.
claimDefine the function $g : ℝ → ℝ$ by $g(x) := x - x^3/3 + x^5/5$.
background
The module supplies constructive interval bounds for arctan and tan via derivative-comparison monotonicity. The upper bound rests on the pointwise inequality (1 - t² + t⁴) ≥ 1/(1 + t²) for t ≥ 0, equivalently 1 + t⁶ ≥ 1, whose antiderivative is the given polynomial. Module documentation states: “For the upper bound: arctan(x) ≤ x − x³/3 + x⁵/5, because (1−t²+t⁴) ≥ 1/(1+t²) (equivalently 1+t⁶ ≥ 1).” Both polynomials are antiderivatives of their bounding functions, and the comparison follows from monotoneOn_of_deriv_nonneg on [0, ∞).
proof idea
The declaration is a direct definition of the polynomial expression. Sibling theorems establish its continuity, differentiability, and explicit derivative by unfolding the definition and applying fun_prop or hasDerivAt calculations on the power terms.
why it matters in Recognition Science
g_upper feeds the inequality arctan_le_upper_poly, which certifies the enclosure arctanOneThirdInterval containing arctan(1/3). This enclosure supports the arctan(2) identity arctan(2) = π/4 + arctan(1/3) proved via Real.arctan_add. The construction supplies the rigorous numerical bounds required for constants in the Recognition framework.
scope and limits
- Does not prove arctan(x) ≤ g_upper(x) for x ≥ 0.
- Does not supply the matching lower-bound polynomial.
- Does not extend the bound to negative arguments.
- Does not compute explicit numerical values or interval enclosures.
Lean usage
theorem arctan_le_g (x : ℝ) (hx : 0 ≤ x) : arctan x ≤ g_upper x := by apply arctan_le_upper_poly x hxformal statement (Lean)
42private noncomputable def g_upper (x : ℝ) : ℝ := x - x ^ 3 / 3 + x ^ 5 / 5
proof body
Definition body.
43