g_upper_deriv
plain-language theorem explainer
The derivative of the upper bounding polynomial g_upper at any real t equals 1 - t² + t⁴. Interval-arithmetic proofs for arctan bounds cite this to justify monotonicity of the error function via the monotone derivative theorem on the nonnegative reals. The proof is a direct term-mode computation that unfolds the polynomial definition, assembles the derivative from power rules, and normalizes the result by ring.
Claim. Let $g(t) := t - t^3/3 + t^5/5$. Then $g$ is differentiable at every real $t$ with $g'(t) = 1 - t^2 + t^4$.
background
The Numerics.Interval.Trig module constructs rigorous interval bounds for arctan by comparing derivatives on [0, ∞). The function g_upper is the explicit antiderivative of the rational upper bound 1 - t² + t⁴; the comparison 1 - t² + t⁴ ≥ 1/(1 + t²) follows from the algebraic identity (1 - t² + t⁴)(1 + t²) = 1 + t⁶ ≥ 1. The module imports basic interval arithmetic (including subtraction) and relies on Mathlib results for arctan continuity, differentiability, and the mean-value theorem.
proof idea
The term proof unfolds the definition of g_upper, then builds the derivative expression by subtracting the scaled cubic power derivative from the identity derivative and adding the scaled quintic power derivative. A single convert tactic with ring normalization confirms that the assembled expression equals 1 - t² + t⁴.
why it matters
This derivative statement is the key step that lets the downstream theorem arctan_le_upper_poly apply monotoneOn_of_deriv_nonneg to the error g_upper(x) - arctan(x). It therefore supplies the constructive upper bound arctan(x) ≤ x - x³/3 + x⁵/5 used throughout the module's trigonometric interval arithmetic, which supports numerical evaluations required by the Recognition Science phi-ladder and constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.