TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Enclosure.Comparison.Runtime

Adaptive comparison with rational enclosures #

The search uses only rational arithmetic. Its termination argument is a proposition and is erased from executable code. Callers supply a sequence of increasingly accurate intervals and a proof that some interval excludes the boundary; real containment is used separately to prove the returned ordering correct.

source
def FloatLib.Numerics.Enclosure.Comparison.Separates (interval : RationalInterval) (boundary : ℚ) :
Prop

An interval lies strictly on one side of a rational boundary.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Numerics.Enclosure.Comparison.instDecidableSeparates (interval : RationalInterval) (boundary : ℚ) :
    Decidable (Separates interval boundary)
    source
    def FloatLib.Numerics.Enclosure.Comparison.compare (intervals : ℕ → RationalInterval) (boundary : ℚ) (terminates : ∃ (n : ℕ), Separates (intervals n) boundary) :
    Ordering

    Search for the first separating interval and return whether it lies below or above the boundary.

    Instances For