arctanTwoInterval
plain-language theorem explainer
The definition constructs a closed rational interval containing arctan(2) by scaling the pi interval by 1/4 and adding the arctan(1/3) interval. Numerics researchers needing rigorous bounds on inverse trigonometric constants would cite it when avoiding floating-point error in Recognition Science computations. The construction is a direct one-line wrapper applying scalar multiplication and interval addition to prior bounds.
Claim. Define the closed interval $I$ with rational endpoints by $I = (1/4)·πInterval + J$, where $J$ is the interval containing arctan(1/3) and πInterval contains π. Then arctan(2) ∈ I.
background
The module supplies constructive interval bounds for arctan using derivative-comparison monotonicity. Interval is the structure with rational lo and hi endpoints satisfying lo ≤ hi. smulPos scales an interval by a positive rational, multiplying both endpoints while preserving validity. piInterval comes from the PiBounds module; arctanOneThirdInterval is the sibling definition for arctan(1/3). From the module documentation: 'All arctan bounds are proved constructively using derivative-comparison monotonicity (monotoneOn_of_deriv_nonneg)'. The arctan(2) identity arctan(2) = π/4 + arctan(1/3) is proved using Real.arctan_add.
proof idea
The definition is a one-line wrapper. It scales piInterval by the positive rational 1/4 via smulPos (with norm_num discharging positivity), then applies interval addition to combine the result with arctanOneThirdInterval.
why it matters
This definition supplies the interval used by the downstream theorem arctan_two_in_interval to prove arctan(2) lies inside it. It completes the constructive bound for arctan(2) inside the trig numerics module, supporting error-free constant computations in the Recognition framework. It relies on the pi bounds and arctan(1/3) interval, fitting the module's use of polynomial antiderivatives and monotone derivative comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.