Rational period reduction for sine and cosine

An enclosed quarter period supplies an approximate full period in [4, 8]. Rounding the quotient to an integer leaves a rational Taylor argument in [-4, 4]. The output radius includes the accumulated period error, using the global Lipschitz bound of sine and cosine. Thus the reduction remains valid even when the selected integer changes as precision grows.

The number of series terms need not grow with the magnitude of the reduced argument. The precision needed in the period still grows with the input magnitude, as expected for range reduction. All arithmetic here is rational; there is no machine approximation to π.

def FloatLib.Numerics.Enclosure.trigQuarter (degree : ℕ) : ℚ

A positive rational approximation to π/4, bounded between one half and one.

def FloatLib.Numerics.Enclosure.trigTurns (x : ℚ) (degree : ℕ) : ℤ

The nearest integer number of approximate full periods, with upward half ties.

def FloatLib.Numerics.Enclosure.trigReducedArgument (x : ℚ) (degree : ℕ) : ℚ

The exact rational remainder after removing the approximate periods.

def FloatLib.Numerics.Enclosure.trigReductionError (x : ℚ) (degree : ℕ) : ℚ

Error from replacing true periods by the rational approximate periods.

def FloatLib.Numerics.Enclosure.trigReducedRadius (x : ℚ) (degree : ℕ) : ℚ

Combined Taylor and period-reduction error.

def FloatLib.Numerics.Enclosure.sinReduced (x : ℚ) (degree : ℕ) : RationalInterval

A sine enclosure with a Taylor argument of magnitude at most four.

def FloatLib.Numerics.Enclosure.cosReduced (x : ℚ) (degree : ℕ) : RationalInterval

A cosine enclosure with the same bounded rational period reduction.