Convergence of rational arctangent bounds

The geometric radius tends to zero on the open series domain. The exact reduction branches depend only on the input, so interval addition, subtraction, scaling, and negation transfer endpoint convergence to every rational argument.

theorem FloatLib.Numerics.Enclosure.tendsto_atanRadius (x : ℚ) (hx : |x| < 1) : Filter.Tendsto (fun (n : ℕ) => ↑(atanRadius x (n + 1))) Filter.atTop (nhds 0)

The arctangent remainder tends to zero throughout the open series domain.

theorem FloatLib.Numerics.Enclosure.tendsto_atanTaylor (x : ℚ) (hx : |x| < 1) : Filter.Tendsto (fun (n : ℕ) => ↑(atanTaylor x (n + 1))) Filter.atTop (nhds (Real.arctan ↑x))

Rational arctangent partial sums converge to the real arctangent.

theorem FloatLib.Numerics.Enclosure.tendsto_atanSmall_lo (x : ℚ) (hx : |x| < 1) : Filter.Tendsto (fun (n : ℕ) => ↑(atanSmall x n).lo) Filter.atTop (nhds (Real.arctan ↑x))

The small arctangent lower endpoints converge to the exact value.

theorem FloatLib.Numerics.Enclosure.tendsto_atanSmall_hi (x : ℚ) (hx : |x| < 1) : Filter.Tendsto (fun (n : ℕ) => ↑(atanSmall x n).hi) Filter.atTop (nhds (Real.arctan ↑x))

The small arctangent upper endpoints converge to the exact value.

theorem FloatLib.Numerics.Enclosure.tendsto_piQuarter_lo : Filter.Tendsto (fun (n : ℕ) => ↑(piQuarter n).lo) Filter.atTop (nhds (Real.pi / 4))

The lower rational bounds for π/4 approach π/4.

theorem FloatLib.Numerics.Enclosure.tendsto_piQuarter_hi : Filter.Tendsto (fun (n : ℕ) => ↑(piQuarter n).hi) Filter.atTop (nhds (Real.pi / 4))

The upper rational bounds for π/4 approach π/4.

theorem FloatLib.Numerics.Enclosure.tendsto_atanUnit_lo (x : ℚ) (hx : 0 ≤ x) (hone : x ≤ 1) : Filter.Tendsto (fun (n : ℕ) => ↑(atanUnit x n).lo) Filter.atTop (nhds (Real.arctan ↑x))

Arctangent reduction on [0, 1] preserves lower-endpoint convergence.

theorem FloatLib.Numerics.Enclosure.tendsto_atanUnit_hi (x : ℚ) (hx : 0 ≤ x) (hone : x ≤ 1) : Filter.Tendsto (fun (n : ℕ) => ↑(atanUnit x n).hi) Filter.atTop (nhds (Real.arctan ↑x))

Arctangent reduction on [0, 1] preserves upper-endpoint convergence.

theorem FloatLib.Numerics.Enclosure.tendsto_atanNonnegative_lo (x : ℚ) (hx : 0 ≤ x) : Filter.Tendsto (fun (n : ℕ) => ↑(atanNonnegative x n).lo) Filter.atTop (nhds (Real.arctan ↑x))

Inversion preserves lower-endpoint convergence for nonnegative inputs.

theorem FloatLib.Numerics.Enclosure.tendsto_atanNonnegative_hi (x : ℚ) (hx : 0 ≤ x) : Filter.Tendsto (fun (n : ℕ) => ↑(atanNonnegative x n).hi) Filter.atTop (nhds (Real.arctan ↑x))

Inversion preserves upper-endpoint convergence for nonnegative inputs.

theorem FloatLib.Numerics.Enclosure.tendsto_atan_lo (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(atan x n).lo) Filter.atTop (nhds (Real.arctan ↑x))

The lower enclosure endpoints converge for every rational arctangent input.

theorem FloatLib.Numerics.Enclosure.tendsto_atan_hi (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(atan x n).hi) Filter.atTop (nhds (Real.arctan ↑x))

The upper enclosure endpoints converge for every rational arctangent input.