Rational enclosures at rational multiples of pi

The angle is reduced modulo two exactly, before multiplication by an enclosed value of pi. Consequently both the Taylor argument and the error multiplier are bounded independently of large integer parts of the input. The radius includes the uncertainty in pi. These operations use neither a rounded value of pi nor an approximate rational-angle equality test.

def FloatLib.Numerics.Enclosure.piTurns (argument : ℚ) : ℤ

Integer full turns removed from a pi-scaled angle, with upward half ties.

def FloatLib.Numerics.Enclosure.piReduced (argument : ℚ) : ℚ

Exact reduction of a pi-scaled angle to [-1, 1).

def FloatLib.Numerics.Enclosure.piArgument (argument : ℚ) (degree : ℕ) : ℚ

A rational Taylor argument obtained from the lower, clamped quarter-period enclosure.

def FloatLib.Numerics.Enclosure.piArgumentError (argument : ℚ) (degree : ℕ) : ℚ

Error introduced by using the rational approximation to pi.

def FloatLib.Numerics.Enclosure.piRadius (argument : ℚ) (degree : ℕ) : ℚ

Combined Taylor remainder and argument uncertainty.

def FloatLib.Numerics.Enclosure.sinPi (argument : ℚ) (degree : ℕ) : RationalInterval

Enclose sin (argument * π) after exact rational angle reduction.

def FloatLib.Numerics.Enclosure.cosPi (argument : ℚ) (degree : ℕ) : RationalInterval

Enclose cos (argument * π) with the same exact angle reduction.

def FloatLib.Numerics.Enclosure.sinPiSubCos (argument boundary : ℚ) (degree : ℕ) : RationalInterval

A division-free enclosure of the residual used to compare pi-scaled tangent.