Global rational sine and cosine bounds

The rational polynomials are identified with real Taylor polynomials at zero. Mathlib's Lagrange remainder theorem applies at every real argument: every iterated derivative of sine or cosine has absolute value at most one. Thus no domain restriction or unproved reduction condition enters the containment theorem.

theorem FloatLib.Numerics.Enclosure.cast_sinCoefficient (n : ℕ) : ↑(sinCoefficient n) = iteratedDeriv n Real.sin 0

Rational sine coefficients are the exact real derivatives at the origin.

theorem FloatLib.Numerics.Enclosure.cast_cosCoefficient (n : ℕ) : ↑(cosCoefficient n) = iteratedDeriv n Real.cos 0

Rational cosine coefficients are the exact real derivatives at the origin.

theorem FloatLib.Numerics.Enclosure.abs_sin_sub_sinTaylor_le (x : ℚ) (degree : ℕ) : |Real.sin ↑x - ↑(sinTaylor x degree)| ≤ ↑(trigRadius x degree)

The executable sine polynomial has a valid remainder bound for every rational input.

theorem FloatLib.Numerics.Enclosure.abs_cos_sub_cosTaylor_le (x : ℚ) (degree : ℕ) : |Real.cos ↑x - ↑(cosTaylor x degree)| ≤ ↑(trigRadius x degree)

The executable cosine polynomial has the same global remainder guarantee.

theorem FloatLib.Numerics.Enclosure.contains_restrictUnit {interval : RationalInterval} {x : ℝ} (hx : interval.Contains x) (hbound : |x| ≤ 1) : (restrictUnit interval).Contains x

Intersecting with [-1, 1] retains containment of any value in that range.

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

Every finite degree provides a sound enclosure of sine on all rational arguments.

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

Every finite degree provides a sound enclosure of cosine on all rational arguments.