Containment after exact rational angle reduction

Removing an integer number of full turns preserves sine and cosine exactly. Their global Lipschitz bounds control the remaining uncertainty in pi, and the usual Taylor remainder then gives a real containment theorem at every degree.

theorem FloatLib.Numerics.Enclosure.abs_piReduced_le (argument : ℚ) : |piReduced argument| ≤ 1

Exact angle reduction bounds the remaining pi-scaled angle by one.

theorem FloatLib.Numerics.Enclosure.abs_piArgument_le (argument : ℚ) (degree : ℕ) : |piArgument argument degree| ≤ 4

The Taylor argument is bounded by four independently of the unreduced input.

theorem FloatLib.Numerics.Enclosure.sin_piReduced (argument : ℚ) : Real.sin (↑(piReduced argument) * Real.pi) = Real.sin (↑argument * Real.pi)

Exact removal of full turns preserves sine.

theorem FloatLib.Numerics.Enclosure.cos_piReduced (argument : ℚ) : Real.cos (↑(piReduced argument) * Real.pi) = Real.cos (↑argument * Real.pi)

Exact removal of full turns preserves cosine.

theorem FloatLib.Numerics.Enclosure.abs_piArgument_sub_le (argument : ℚ) (degree : ℕ) : |↑(piArgument argument degree) - ↑(piReduced argument) * Real.pi| ≤ ↑(piArgumentError argument degree)

The rational approximation error bounds distance from the exact reduced angle.

theorem FloatLib.Numerics.Enclosure.abs_sinPi_sub_sinArgument_le (argument : ℚ) (degree : ℕ) : |Real.sin (↑argument * Real.pi) - Real.sin ↑(piArgument argument degree)| ≤ ↑(piArgumentError argument degree)

The argument uncertainty transfers through sine by its global Lipschitz bound.

theorem FloatLib.Numerics.Enclosure.abs_cosPi_sub_cosArgument_le (argument : ℚ) (degree : ℕ) : |Real.cos (↑argument * Real.pi) - Real.cos ↑(piArgument argument degree)| ≤ ↑(piArgumentError argument degree)

The argument uncertainty transfers through cosine by its global Lipschitz bound.

theorem FloatLib.Numerics.Enclosure.abs_sinPi_sub_taylor_le (argument : ℚ) (degree : ℕ) : |Real.sin (↑argument * Real.pi) - ↑(sinTaylor (piArgument argument degree) degree)| ≤ ↑(piRadius argument degree)

Taylor and argument errors together bound the pi-scaled sine polynomial.

theorem FloatLib.Numerics.Enclosure.abs_cosPi_sub_taylor_le (argument : ℚ) (degree : ℕ) : |Real.cos (↑argument * Real.pi) - ↑(cosTaylor (piArgument argument degree) degree)| ≤ ↑(piRadius argument degree)

Taylor and argument errors together bound the pi-scaled cosine polynomial.

theorem FloatLib.Numerics.Enclosure.contains_sinPi (argument : ℚ) (degree : ℕ) : (sinPi argument degree).Contains (Real.sin (↑argument * Real.pi))

Every sine enclosure contains the exact value, including rational-angle special values.

theorem FloatLib.Numerics.Enclosure.contains_cosPi (argument : ℚ) (degree : ℕ) : (cosPi argument degree).Contains (Real.cos (↑argument * Real.pi))

Every cosine enclosure contains the exact value.