h_lower_differentiable
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.