TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Interval.RealBounds

Real interval corner bounds #

The ordered-field proofs live in Numerics.Enclosure.Interval.Bounds. These real-specialized names preserve the interval API used by floating-point model semantics.

source
def FloatLib.Floats.Interval.minOfFour {α : Type u_1} [LinearOrder α] (a b c d : α) :
α

Minimum of four values with the grouping used by interval corner calculations.

Instances For
    source
    def FloatLib.Floats.Interval.maxOfFour {α : Type u_1} [LinearOrder α] (a b c d : α) :
    α

    Maximum of four values with the grouping used by interval corner calculations.

    Instances For
      source
      theorem FloatLib.Floats.Interval.mul_bounds_Icc (a b c d x y : ℝ) (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc c d) :
      x * y ∈ Set.Icc (minOfFour (a * c) (a * d) (b * c) (b * d)) (maxOfFour (a * c) (a * d) (b * c) (b * d))

      Four-corner enclosure of a real product.

      source
      theorem FloatLib.Floats.Interval.div_bounds_Icc (a b c d x y : ℝ) (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc c d) (hzero : d < 0 ∨ 0 < c) :
      x / y ∈ Set.Icc (minOfFour (a / c) (a / d) (b / c) (b / d)) (maxOfFour (a / c) (a / d) (b / c) (b / d))

      Four-corner enclosure of a real quotient when the denominator interval excludes zero.