TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Floats.Interval.Arb

Arb-backed enclosures with configured endpoints #

Arb/python-flint supplies the external real-enclosure claim. Exact rational endpoints are then rounded by FloatLib's descriptor-generic software rounders and packed through the selected ModelCodec. For IEEE formats, the transport theorems prove that conversion rounds outward, including overflow to infinite endpoints.

These theorems cover endpoint conversion only. They do not state that unary returns an enclosure of the requested function: Arb's answer remains unchecked. No native floating-point conversion or software transcendental approximation participates in the endpoint conversion.

source
theorem TorchLean.Floats.Interval.Arb.toEReal_roundRatQDown_le {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (q : ℚ) (hformat : format.isIEEE = true) :
(FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.ofRat format q FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.down)).toModel.toEReal ≤ ↑↑q

Packing the downward rational conversion preserves its extended-real lower bound.

source
theorem TorchLean.Floats.Interval.Arb.toEReal_roundRatQUp_ge {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (q : ℚ) (hformat : format.isIEEE = true) :
↑↑q ≤ (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.ofRat format q FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.up)).toModel.toEReal

Packing the upward rational conversion preserves its extended-real upper bound.

source
def TorchLean.Floats.Interval.Arb.finite {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (x : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)) (label : String) :
IO ℚ

Decode an endpoint exactly as a rational, failing on NaN or infinity.

Instances For
    source
    def TorchLean.Floats.Interval.Arb.bounds {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (func : String) (X : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan))) (precBits digits : ℕ := 200) :
    IO (ℚ × ℚ)

    Send exact rational input endpoints to Arb and return its claimed rational enclosure.

    Non-finite inputs fail before the request. This call crosses the external oracle trust boundary; parsing its response does not prove that the requested function lies within these bounds.

    Instances For
      source
      def TorchLean.Floats.Interval.Arb.unary {format : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model format) code] (func : String) (X : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan))) (precBits digits : ℕ := 200) :
      IO (FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family format code plan)))

      Round Arb's claimed enclosure for a unary function into the input's format and storage plan.

      For format.isIEEE = true, the endpoint transport theorems prove outward rounding, including overflow. Enclosure of the requested function still depends on Arb's external claim.

      Instances For