arctanTwoInterval
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not compute a numerical approximation to arctan(2).
- Does not establish the identity arctan(2) = π/4 + arctan(1/3) itself.
- Does not extend the construction to arctan of other arguments.
- Does not claim tighter bounds than the sum of the component intervals.
Lean usage
theorem arctan_two_in_interval : arctanTwoInterval.contains (arctan 2) := by rw [arctan_two_eq]; unfold arctanTwoInterval; apply add_contains_addformal statement (Lean)
161def arctanTwoInterval : Interval :=
proof body
Definition body.
162 let pi4 := smulPos (1 / 4) piInterval (by norm_num)
163 add pi4 arctanOneThirdInterval
164
165/-- **PROVED**: arctan(2) is in arctanTwoInterval. -/