h_lower_differentiable
The theorem asserts that the lower bounding polynomial for arctan remains differentiable over the reals. Analysts building monotonicity arguments for arctan minus its approximant cite this to license derivative comparison on [0, ∞). Proof reduces to a one-line wrapper that unfolds the polynomial definition and applies a general differentiability tactic.
claimThe function $h(x) := x - x^3/3 + x^5/5 - x^7/7$ is differentiable on $ℝ$.
background
The module develops constructive interval bounds for arctan(x) on [0, ∞) by comparing derivatives of the target function against explicit polynomials. The lower bound rests on the polynomial whose derivative is 1 - t² + t⁴ - t⁶, shown algebraically to lie below 1/(1 + t²) because 1 - t⁸ ≤ 1. MonotoneOn_of_deriv_nonneg then integrates the comparison to obtain the desired inequality between arctan and its approximant.
proof idea
One-line wrapper that unfolds the definition of h_lower and invokes the fun_prop tactic to conclude differentiability over the reals.
why it matters in Recognition Science
The result supplies the differentiability hypothesis required by lower_poly_le_arctan, which establishes the concrete lower bound arctan(x) ≥ h_lower(x) for x ≥ 0. It thereby supports the module's derivative-comparison strategy for rigorous, constructive arctan bounds without appeal to non-constructive existence statements.
scope and limits
- Does not compute or display the explicit derivative formula.
- Does not prove the arctan inequality itself.
- Applies only to this specific polynomial on the reals.
- Does not address complex arctan or other trigonometric functions.
formal statement (Lean)
84private theorem h_lower_differentiable : Differentiable ℝ h_lower := by unfold h_lower; fun_prop
proof body
85