Convergence of global rational sine and cosine bounds

For every fixed real argument, the exponential-series terms |x|^n / n! tend to zero. The global Taylor error bound therefore squeezes the rational sine and cosine polynomials toward their exact values. Intersecting with [-1, 1] preserves endpoint convergence.

theorem FloatLib.Numerics.Enclosure.tendsto_trigRadius (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(trigRadius x n)) Filter.atTop (nhds 0)

The global trigonometric Lagrange radius tends to zero at every rational input.

theorem FloatLib.Numerics.Enclosure.tendsto_sinTaylor (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(sinTaylor x n)) Filter.atTop (nhds (Real.sin ↑x))

The executable sine Taylor polynomials converge at every rational input.

theorem FloatLib.Numerics.Enclosure.tendsto_cosTaylor (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(cosTaylor x n)) Filter.atTop (nhds (Real.cos ↑x))

The executable cosine Taylor polynomials converge at every rational input.

theorem FloatLib.Numerics.Enclosure.tendsto_restrictUnit_lo {α : Type u_1} {l : Filter α} {intervals : α → RationalInterval} {x : ℝ} (hlo : Filter.Tendsto (fun (a : α) => ↑(intervals a).lo) l (nhds x)) (hx : -1 ≤ x) : Filter.Tendsto (fun (a : α) => ↑(restrictUnit (intervals a)).lo) l (nhds x)

Clamping lower endpoints at -1 preserves any limit at least -1.

theorem FloatLib.Numerics.Enclosure.tendsto_restrictUnit_hi {α : Type u_1} {l : Filter α} {intervals : α → RationalInterval} {x : ℝ} (hhi : Filter.Tendsto (fun (a : α) => ↑(intervals a).hi) l (nhds x)) (hx : x ≤ 1) : Filter.Tendsto (fun (a : α) => ↑(restrictUnit (intervals a)).hi) l (nhds x)

Clamping upper endpoints at 1 preserves any limit at most 1.

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

The sine lower endpoints converge globally as the degree increases.

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

The sine upper endpoints converge globally as the degree increases.

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

The cosine lower endpoints converge globally as the degree increases.

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

The cosine upper endpoints converge globally as the degree increases.