Convergence of pi-scaled trigonometric enclosures

The exact rational angle reduction is independent of the refinement degree. Its bounded remainder multiplies a vanishing uncertainty in pi, while a uniform factorial majorant controls the Taylor error. Thus both endpoints converge at every rational input, including special angles where a later comparison must use the exact-value classifier.

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

The argument uncertainty vanishes at every rational pi-scaled input.

theorem FloatLib.Numerics.Enclosure.trigRadius_piArgument_le (x : ℚ) (degree : ℕ) : trigRadius (piArgument x degree) degree ≤ trigRadius 4 degree

The bounded reduced arguments give a uniform factorial majorant for the Taylor error.

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

The reduced Taylor error tends to zero even though its rational argument varies.

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

The complete radius of the reduced enclosure tends to zero.

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

Reduced sine polynomials converge to the sine of the original argument.

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

Reduced cosine polynomials converge to the cosine of the original argument.

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

The reduced sine lower endpoints converge at every rational input.

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

The reduced sine upper endpoints converge at every rational input.

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

The reduced cosine lower endpoints converge at every rational input.

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

The reduced cosine upper endpoints converge at every rational input.