arctanOneThirdInterval
Definition of the rational interval [0.321, 0.322] that encloses arctan(1/3). Numerics researchers in Recognition Science cite it when building rigorous enclosures for arctangent in interval arithmetic. The definition is a direct construction of an Interval structure with rational endpoints and a norm_num validity check.
claimThe closed interval $[321/1000, 322/1000]$ containing $arctan(1/3)$.
background
Interval is the structure from Numerics.Interval.Basic with rational fields lo and hi together with a proof that lo ≤ hi. The module develops constructive bounds for arctan via derivative-comparison monotonicity on [0, ∞): the upper polynomial satisfies arctan(x) ≤ x − x³/3 + x⁵/5 because (1 − t² + t⁴) ≥ 1/(1 + t²), while the lower polynomial satisfies x − x³/3 + x⁵/5 − x⁷/7 ≤ arctan(x) because (1 − t² + t⁴ − t⁶) ≤ 1/(1 + t²). These antiderivatives and comparisons are obtained from monotoneOn_of_deriv_nonneg.
proof idea
Direct definition that instantiates the Interval structure with the two rational endpoints and applies the norm_num tactic to discharge the lo ≤ hi obligation. No lemmas beyond the structure definition are required.
why it matters in Recognition Science
Supplies the enclosure for arctan(1/3) that is invoked by the containment theorem arctan_one_third_in_interval and by the definition of arctanTwoInterval, which in turn uses the identity arctan(2) = π/4 + arctan(1/3). It therefore participates in the module's program of rigorous, constructive interval arithmetic for trigonometric functions that supports exact computations inside the Recognition framework.
scope and limits
- Does not compute the exact numerical value of arctan(1/3).
- Does not supply enclosures for arctan at arguments other than 1/3.
- Does not incorporate floating-point rounding analysis.
Lean usage
def arctanTwoInterval : Interval := let pi4 := smulPos (1 / 4) piInterval (by norm_num); add pi4 arctanOneThirdIntervalformal statement (Lean)
122def arctanOneThirdInterval : Interval where
123 lo := 321 / 1000 -- 0.321
proof body
Definition body.
124 hi := 322 / 1000 -- 0.322
125 valid := by norm_num
126
127/-- **PROVED**: arctan(1/3) is in arctanOneThirdInterval.
128 Lower bound from `h_lower(1/3) = 24628/76545 ≥ 321/1000`.
129 Upper bound from `g_upper(1/3) = 391/1215 ≤ 322/1000`. -/