Real containment for interval elementary functions

Endpoint monotonicity proves the exponential, logarithm, arctangent, and square-root bounds. The sine and cosine proofs use Mathlib's global Lipschitz estimates, so their intervals remain valid across extrema. The square-root proof reduces to Nat.sqrt_le' and Nat.lt_succ_sqrt'. No theorem restricts an interval's members to rational values.

theorem FloatLib.Numerics.Interval.containsReal_monotoneBounds (enclose : ℚ → Interval ℚ) (f : ℝ → ℝ) (I : Interval ℚ) (hf : MonotoneOn f (Set.Icc ↑I.lo ↑I.hi)) (henclose : ∀ q ∈ Set.Icc I.lo I.hi, ContainsReal some (enclose q) (f ↑q)) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some (monotoneBounds enclose I) (f x)

Point enclosures and monotonicity on the input interval enclose its entire real image.

theorem FloatLib.Numerics.Interval.containsReal_expBounds (I : Interval ℚ) (terms : ℕ) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some (I.expBounds terms) (Real.exp x)

The exponential bounds contain exp x for every real member of the input interval.

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

A successful logarithm enclosure contains the logarithm of every enclosed real value.

theorem FloatLib.Numerics.Interval.containsReal_atanBounds (I : Interval ℚ) (terms : ℕ) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some (I.atanBounds terms) (Real.arctan x)

The arctangent bounds contain the image of every enclosed real value.

theorem FloatLib.Numerics.Interval.containsReal_lipschitzUnitBounds (enclose : ℚ → Interval ℚ) (f : ℝ → ℝ) (hf : LipschitzWith 1 f) (hrange : ∀ (x : ℝ), |f x| ≤ 1) (henclose : ∀ (q : ℚ), ContainsReal some (enclose q) (f ↑q)) (I : Interval ℚ) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some (lipschitzUnitBounds enclose I) (f x)

A unit-Lipschitz function is enclosed by its midpoint bounds plus the half-width.

theorem FloatLib.Numerics.Interval.containsReal_sinBounds (I : Interval ℚ) (terms : ℕ) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some (I.sinBounds terms) (Real.sin x)

Sine containment holds throughout the interval, including interior extrema.

theorem FloatLib.Numerics.Interval.containsReal_cosBounds (I : Interval ℚ) (terms : ℕ) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some (I.cosBounds terms) (Real.cos x)

Cosine containment holds throughout the interval, including interior extrema.

theorem FloatLib.Numerics.Interval.containsReal_sqrtPointBounds (x : ℚ) (precision : ℕ) (hx : 0 ≤ x) : ContainsReal some (sqrtPointBounds x precision) √↑x

Integer square-root bounds enclose the real square root of every nonnegative rational.

theorem FloatLib.Numerics.Interval.sqrtPointBounds_width_le (x : ℚ) (precision : ℕ) : (sqrtPointBounds x precision).hi - (sqrtPointBounds x precision).lo ≤ 1 / 2 ^ precision

The point square-root enclosure is at most one dyadic grid step wide.

theorem FloatLib.Numerics.Interval.containsReal_sqrtBounds? {I K : Interval ℚ} {precision : ℕ} (h : I.sqrtBounds? precision = some K) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal some K √x

Successful dyadic square-root bounds contain the image of every enclosed real value.