Real containment for interval arcsine and arccosine

Mathlib's Real.arcsin_eq_arctan connects interior point enclosures to arcsine. Its monotonicity theorem then bounds every real member of an interval by the endpoint images. The cases at -1 and 1 use the existing enclosure of π/4. Arccosine containment follows from Real.arccos_eq_pi_div_two_sub_arcsin.

@[simp]

theorem FloatLib.Numerics.Interval.asinBounds?_point_zero (terms precision : ℕ) : (point 0).asinBounds? terms precision = some (point 0)

Arcsine preserves exact zero independently of both accuracy parameters.

@[simp]

theorem FloatLib.Numerics.Interval.acosBounds?_point_one (terms precision : ℕ) : (point 1).acosBounds? terms precision = some (point 0)

Arccosine at one is exactly zero independently of both accuracy parameters.

theorem FloatLib.Numerics.Interval.Internal.containsReal_asinPointBounds? {q : ℚ} {terms precision : ℕ} {K : Interval ℚ} (h : asinPointBounds? q terms precision = some K) : ContainsReal some K (Real.arcsin ↑q)

A successful point enclosure contains the real arcsine, including at both endpoints.

theorem FloatLib.Numerics.Interval.containsReal_asinBounds? {I K : Interval ℚ} {terms precision : ℕ} (h : I.asinBounds? terms precision = some K) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some K (Real.arcsin x)

Successful arcsine bounds contain the image of every real member of the input interval.

theorem FloatLib.Numerics.Interval.containsReal_acosBounds? {I K : Interval ℚ} {terms precision : ℕ} (h : I.acosBounds? terms precision = some K) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some K (Real.arccos x)

Successful arccosine bounds contain the image of every real member of the input interval.