Correctness of rational trigonometric period reduction

The approximate remainder is bounded independently of the input. Its distance from a true period translate is bounded by the explicit rational reduction error. Periodicity and the Lipschitz estimates then transfer the Taylor enclosure to the original argument.

theorem FloatLib.Numerics.Enclosure.half_le_trigQuarter (degree : ℕ) : 1 / 2 ≤ trigQuarter degree

The rational quarter period is at least one half.

theorem FloatLib.Numerics.Enclosure.trigQuarter_le_one (degree : ℕ) : trigQuarter degree ≤ 1

The rational quarter period is at most one.

theorem FloatLib.Numerics.Enclosure.trigQuarter_le_pi_quarter (degree : ℕ) : ↑(trigQuarter degree) ≤ Real.pi / 4

The rational quarter period lies below the true quarter period.

theorem FloatLib.Numerics.Enclosure.trigQuarter_le_hi (degree : ℕ) : trigQuarter degree ≤ (piQuarter degree).hi

The upper quarter-period endpoint lies above the clamped lower approximation.

theorem FloatLib.Numerics.Enclosure.abs_trig_turns_residual_le (x : ℚ) (degree : ℕ) : |x / (8 * trigQuarter degree) - ↑(trigTurns x degree)| ≤ 1 / 2

Rounding to the nearest integer leaves at most half a period.

theorem FloatLib.Numerics.Enclosure.abs_trigReducedArgument_le (x : ℚ) (degree : ℕ) : |trigReducedArgument x degree| ≤ 4

Every reduced rational argument lies in [-4, 4], regardless of input magnitude.

theorem FloatLib.Numerics.Enclosure.abs_trigTurns_le (x : ℚ) (degree : ℕ) : |↑(trigTurns x degree)| ≤ |x| + 1

The number of removed periods has a uniform bound as the degree varies.

theorem FloatLib.Numerics.Enclosure.trigReductionError_nonneg (x : ℚ) (degree : ℕ) : 0 ≤ trigReductionError x degree

The accumulated rational period error is nonnegative.

theorem FloatLib.Numerics.Enclosure.trigReductionError_le (x : ℚ) (degree : ℕ) : trigReductionError x degree ≤ 8 * (|x| + 1) * ((piQuarter degree).hi - trigQuarter degree)

An input-dependent constant times the quarter-period width bounds the reduction error.

theorem FloatLib.Numerics.Enclosure.abs_trigReducedArgument_sub_period_le (x : ℚ) (degree : ℕ) : |↑(trigReducedArgument x degree) - (↑x - ↑(trigTurns x degree) * (2 * Real.pi))| ≤ ↑(trigReductionError x degree)

The approximate remainder is close to an exact integer translate by 2π.

theorem FloatLib.Numerics.Enclosure.abs_sin_sub_reduced_le (x : ℚ) (degree : ℕ) : |Real.sin ↑x - Real.sin ↑(trigReducedArgument x degree)| ≤ ↑(trigReductionError x degree)

The sine error introduced by rational period reduction is explicitly bounded.

theorem FloatLib.Numerics.Enclosure.abs_cos_sub_reduced_le (x : ℚ) (degree : ℕ) : |Real.cos ↑x - Real.cos ↑(trigReducedArgument x degree)| ≤ ↑(trigReductionError x degree)

The cosine error introduced by rational period reduction is explicitly bounded.

theorem FloatLib.Numerics.Enclosure.abs_sin_sub_reducedTaylor_le (x : ℚ) (degree : ℕ) : |Real.sin ↑x - ↑(sinTaylor (trigReducedArgument x degree) degree)| ≤ ↑(trigReducedRadius x degree)

Combined period and Taylor errors bound the sine polynomial at the reduced argument.

theorem FloatLib.Numerics.Enclosure.abs_cos_sub_reducedTaylor_le (x : ℚ) (degree : ℕ) : |Real.cos ↑x - ↑(cosTaylor (trigReducedArgument x degree) degree)| ≤ ↑(trigReducedRadius x degree)

Combined period and Taylor errors bound the cosine polynomial at the reduced argument.

theorem FloatLib.Numerics.Enclosure.contains_sinReduced (x : ℚ) (degree : ℕ) : (sinReduced x degree).Contains (Real.sin ↑x)

The reduced sine enclosure contains the exact sine at every rational input and degree.

theorem FloatLib.Numerics.Enclosure.contains_cosReduced (x : ℚ) (degree : ℕ) : (cosReduced x degree).Contains (Real.cos ↑x)

The reduced cosine enclosure contains the exact cosine at every rational input and degree.