g_upper_continuous
The theorem asserts continuity of the upper bounding polynomial g(x) = x - x³/3 + x⁵/5 on the reals. Analysts building rigorous interval enclosures for arctan cite this when applying derivative monotonicity arguments that require continuousOn. The proof is a one-line wrapper that unfolds the definition and delegates to the fun_prop tactic.
claimThe function $g(x) = x - x^3/3 + x^5/5$ is continuous.
background
This module supplies constructive interval bounds for arctan via polynomial comparisons obtained from derivative tests. The upper bound polynomial is the antiderivative of 1 - t² + t⁴, which dominates 1/(1 + t²) on [0, ∞). The local setting uses Mathlib's monotoneOn_of_deriv_nonneg to turn the pointwise inequality into the global bound arctan(x) ≤ g_upper(x) for x ≥ 0.
proof idea
The proof is a one-line wrapper: it unfolds the definition of g_upper and invokes the fun_prop tactic, which automatically confirms continuity of the resulting polynomial.
why it matters in Recognition Science
This continuity statement is invoked inside the proof of arctan_le_upper_poly to obtain the continuousOn hypothesis needed for monotoneOn_of_deriv_nonneg on the difference g_upper - arctan. It therefore closes a technical prerequisite in the constructive arctan bound chain that supports numerical verification of constants such as π and α.
scope and limits
- Does not establish any error bounds between g_upper and arctan.
- Does not prove differentiability of g_upper.
- Does not extend the result to complex arguments.
formal statement (Lean)
44private theorem g_upper_continuous : Continuous g_upper := by unfold g_upper; fun_prop