Soundness and termination of hyperbolic enclosures

The rational endpoints converge to the mathematical hyperbolic sine and cosine. At a nonzero rational argument neither result is rational: otherwise its exponential would satisfy a nonzero quadratic polynomial over the rationals, contradicting transcendence. Thus adaptive comparison eventually separates every rational boundary.

theorem FloatLib.Numerics.Enclosure.contains_sinh (x : ℚ) (degree : ℕ) : (sinh x degree).Contains (Real.sinh ↑x)

The rational hyperbolic sine interval contains the exact real value.

theorem FloatLib.Numerics.Enclosure.contains_cosh (x : ℚ) (degree : ℕ) : (cosh x degree).Contains (Real.cosh ↑x)

The rational hyperbolic cosine interval contains the exact real value.

theorem FloatLib.Numerics.Enclosure.tendsto_sinh_lo (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(sinh x n).lo) Filter.atTop (nhds (Real.sinh ↑x))

Lower hyperbolic sine endpoints converge to the exact real value.

theorem FloatLib.Numerics.Enclosure.tendsto_sinh_hi (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(sinh x n).hi) Filter.atTop (nhds (Real.sinh ↑x))

Upper hyperbolic sine endpoints converge to the exact real value.

theorem FloatLib.Numerics.Enclosure.tendsto_cosh_lo (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(cosh x n).lo) Filter.atTop (nhds (Real.cosh ↑x))

Lower hyperbolic cosine endpoints converge to the exact real value.

theorem FloatLib.Numerics.Enclosure.tendsto_cosh_hi (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(cosh x n).hi) Filter.atTop (nhds (Real.cosh ↑x))

Upper hyperbolic cosine endpoints converge to the exact real value.

theorem FloatLib.Numerics.Enclosure.sinh_ratCast_ne_ratCast (x q : ℚ) (hx : x ≠ 0) : Real.sinh ↑x ≠ ↑q

A nonzero rational argument cannot have a rational hyperbolic sine.

theorem FloatLib.Numerics.Enclosure.cosh_ratCast_ne_ratCast (x q : ℚ) (hx : x ≠ 0) : Real.cosh ↑x ≠ ↑q

A nonzero rational argument cannot have a rational hyperbolic cosine.

theorem FloatLib.Numerics.Enclosure.exists_sinh_separating (argument boundary : ℚ) (hne : argument ≠ 0) : ∃ (n : ℕ), Comparison.Separates (sinh argument (2 ^ n)) boundary

Doubling the degree eventually separates every rational hyperbolic sine boundary.

theorem FloatLib.Numerics.Enclosure.exists_cosh_separating (argument boundary : ℚ) (hne : argument ≠ 0) : ∃ (n : ℕ), Comparison.Separates (cosh argument (2 ^ n)) boundary

Doubling the degree eventually separates every rational hyperbolic cosine boundary.