Containment for rational arctangent enclosures

Mathlib's real arctangent series identifies the exact sum. Its geometric tail estimate bounds the rational partial sums. The reduction identities hold over the reals; rational interval arithmetic preserves their exact constants.

theorem FloatLib.Numerics.Enclosure.cast_atanTaylor (x : ℚ) (n : ℕ) : ↑(atanTaylor x n) = ∑ i ∈ Finset.range n, (-1) ^ i * ↑x ^ (2 * i + 1) / (2 * ↑i + 1)

Casting the executable polynomial gives the usual real arctangent partial sum.

theorem FloatLib.Numerics.Enclosure.cast_atanRadius (x : ℚ) (n : ℕ) : ↑(atanRadius x n) = |↑x| * (↑x ^ 2) ^ n / (1 - ↑x ^ 2)

The exact rational radius agrees with its real geometric expression.

theorem FloatLib.Numerics.Enclosure.norm_atan_term_le (x : ℝ) (n : ℕ) : ‖(-1) ^ n * x ^ (2 * n + 1) / (2 * ↑n + 1)‖ ≤ |x| * (x ^ 2) ^ n

The geometric majorant bounds every arctangent series term in absolute value.

theorem FloatLib.Numerics.Enclosure.abs_atan_sub_atanTaylor_le (x : ℚ) (n : ℕ) (hx : |x| < 1) : |Real.arctan ↑x - ↑(atanTaylor x n)| ≤ ↑(atanRadius x n)

Every finite-degree arctangent approximation has a valid absolute-error bound.

theorem FloatLib.Numerics.Enclosure.contains_atanSmall (x : ℚ) (degree : ℕ) (hx : |x| < 1) : (atanSmall x degree).Contains (Real.arctan ↑x)

The small kernel contains the true arctangent throughout its open series domain.

theorem FloatLib.Numerics.Enclosure.contains_piQuarter (degree : ℕ) : (piQuarter degree).Contains (Real.pi / 4)

Machin's formula combines the two arctangent enclosures into an enclosure of π/4.

theorem FloatLib.Numerics.Enclosure.abs_atan_unit_argument_le (x : ℚ) (hx : 1 / 2 ≤ x) (hone : x ≤ 1) : |(x - 1) / (x + 1)| ≤ 1 / 3

The transformed argument has magnitude at most one third for 1/2 ≤ x ≤ 1.

theorem FloatLib.Numerics.Enclosure.atan_unit_identity (x : ℚ) (hx : 0 ≤ x) : Real.pi / 4 + Real.arctan ↑((x - 1) / (x + 1)) = Real.arctan ↑x

Adding π/4 to the transformed arctangent recovers the arctangent of any nonnegative input.

theorem FloatLib.Numerics.Enclosure.contains_atanUnit (x : ℚ) (degree : ℕ) (hx : 0 ≤ x) (hone : x ≤ 1) : (atanUnit x degree).Contains (Real.arctan ↑x)

Unit reduction retains real containment, including the switch at one half.

theorem FloatLib.Numerics.Enclosure.contains_atanNonnegative (x : ℚ) (degree : ℕ) (hx : 0 ≤ x) : (atanNonnegative x degree).Contains (Real.arctan ↑x)

Inversion restores the arctangent of every nonnegative rational input.

theorem FloatLib.Numerics.Enclosure.contains_atan (x : ℚ) (degree : ℕ) : (atan x degree).Contains (Real.arctan ↑x)

Every rational input and every finite degree yield a valid arctangent enclosure.