Containment for tangent and hyperbolic interval bounds

The tangent proof composes the existing sine, cosine, and division contracts. Hyperbolic sine is monotone; hyperbolic cosine is monotone on absolute values. Hyperbolic tangent uses the increasing map (u - 1) / (u + 1) on nonnegative exponential values, keeping its denominator strictly positive even when a coarse exponential enclosure has lower endpoint zero.

theorem FloatLib.Numerics.Interval.containsReal_tanBounds? {I K : Interval ℚ} {terms : ℕ} (h : I.tanBounds? terms = some K) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some K (Real.tan x)

Successful tangent bounds contain the tangent of every real member of the input.

theorem FloatLib.Numerics.Interval.containsReal_sinhBounds (I : Interval ℚ) (terms : ℕ) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some (I.sinhBounds terms) (Real.sinh x)

Hyperbolic sine bounds contain the image of every real member of the input.

theorem FloatLib.Numerics.Interval.containsReal_coshBounds (I : Interval ℚ) (terms : ℕ) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some (I.coshBounds terms) (Real.cosh x)

Hyperbolic cosine bounds retain the minimum at zero and contain the whole real image.

theorem FloatLib.Numerics.Interval.containsReal_tanhBounds (I : Interval ℚ) (terms : ℕ) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some (I.tanhBounds terms) (Real.tanh x)

Hyperbolic tangent bounds contain every real image without a denominator-domain failure.