TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Enclosure.Rational.Proof

Soundness of rational interval operations #

Contains interprets executable rational endpoints as a closed real interval. The arithmetic lemmas propagate membership without imposing a floating-point format or rounding policy.

source
def FloatLib.Numerics.RationalInterval.Contains (interval : RationalInterval) (x : ℝ) :
Prop

A real value lies between the rational endpoints.

Instances For
    source
    theorem FloatLib.Numerics.RationalInterval.lo_le_hi {interval : RationalInterval} {x : ℝ} (hx : interval.Contains x) :
    interval.lo ≤ interval.hi

    Every nonempty interval has ordered rational endpoints.

    source
    theorem FloatLib.Numerics.RationalInterval.contains_point (x : ℚ) :
    (point x).Contains ↑x

    A point interval contains its exact rational value.

    source
    theorem FloatLib.Numerics.RationalInterval.contains_around {x : ℝ} {midpoint radius : ℚ} (herror : |x - ↑midpoint| ≤ ↑radius) :
    (around midpoint radius).Contains x

    An absolute-error estimate gives membership in a midpoint-radius interval.

    source
    theorem FloatLib.Numerics.RationalInterval.contains_neg {interval : RationalInterval} {x : ℝ} (hx : interval.Contains x) :
    interval.neg.Contains (-x)

    Negating an enclosed real value reverses the endpoint inequalities.

    source
    theorem FloatLib.Numerics.RationalInterval.contains_add {left right : RationalInterval} {x y : ℝ} (hx : left.Contains x) (hy : right.Contains y) :
    (left.add right).Contains (x + y)

    Addition preserves enclosure.

    source
    theorem FloatLib.Numerics.RationalInterval.contains_sub {left right : RationalInterval} {x y : ℝ} (hx : left.Contains x) (hy : right.Contains y) :
    (left.sub right).Contains (x - y)

    Subtraction preserves enclosure.

    source
    theorem FloatLib.Numerics.RationalInterval.contains_scaleNonnegative {interval : RationalInterval} {x : ℝ} (hx : interval.Contains x) {factor : ℚ} (hfactor : 0 ≤ factor) :
    (interval.scaleNonnegative factor).Contains (↑factor * x)

    A nonnegative rational scale preserves the endpoint inequalities.

    source
    theorem FloatLib.Numerics.RationalInterval.contains_scale {interval : RationalInterval} {x : ℝ} (hx : interval.Contains x) (factor : ℚ) :
    (interval.scale factor).Contains (↑factor * x)

    Signed rational scaling preserves enclosure with the appropriate endpoint order.

    source
    theorem FloatLib.Numerics.RationalInterval.contains_squareNonnegative {interval : RationalInterval} {x : ℝ} (hx : interval.Contains x) (hnonnegative : 0 ≤ x) :
    interval.squareNonnegative.Contains (x ^ 2)

    Squaring a nonnegative enclosed value preserves enclosure.

    source
    theorem FloatLib.Numerics.RationalInterval.contains_squareRepeat {interval : RationalInterval} {x : ℝ} (hx : interval.Contains x) (hnonnegative : 0 ≤ x) (n : ℕ) :
    (interval.squareRepeat n).Contains (x ^ 2 ^ n)

    Repeated squaring encloses the corresponding power of a nonnegative real value.