Convergence with rational period reduction

The integer quotient need not stabilize. Its magnitude has an input-dependent bound, so the vanishing quarter-period uncertainty still makes the reduction error tend to zero. Meanwhile the Taylor radius is uniformly bounded by 4^(n+1)/(n+1)!. These estimates prove endpoint convergence for the executable reduced kernels at every rational input.

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

Clamping the approximate quarter period preserves its limit.

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

The accumulated period error tends to zero without requiring quotient stability.

theorem FloatLib.Numerics.Enclosure.trigRadius_reduced_le (x : ℚ) (degree : ℕ) : trigRadius (trigReducedArgument 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_reduced (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(trigRadius (trigReducedArgument 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_trigReducedRadius (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(trigReducedRadius x n)) Filter.atTop (nhds 0)

The complete radius of the reduced enclosure tends to zero.

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

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

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

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

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

The reduced sine lower endpoints converge at every rational input.

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

The reduced sine upper endpoints converge at every rational input.

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

The reduced cosine lower endpoints converge at every rational input.

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

The reduced cosine upper endpoints converge at every rational input.