TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Enclosure.Rational.Runtime

Executable rational intervals #

The endpoints stay rational throughout a calculation, with no rounding in these operations. Callers use the bounds to compare an exact value with rounding boundaries or to establish a unique rounded result. Soundness over the reals is proved in Rational.Proof.

An interval may be empty: the carrier records endpoints without enforcing their order. Membership hypotheses supply the required ordering in proofs.

source
structure FloatLib.Numerics.RationalInterval :
Type

Closed rational endpoints used to enclose a real value.

  • lo : ℚ

    Lower endpoint.

  • hi : ℚ

    Upper endpoint.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Numerics.instDecidableEqRationalInterval :
    DecidableEq RationalInterval
    source
    def FloatLib.Numerics.instDecidableEqRationalInterval.decEq (x✝ x✝¹ : RationalInterval) :
    Decidable (x✝ = x✝¹)
    Instances For
      source
      def FloatLib.Numerics.instReprRationalInterval.repr :
      RationalInterval → ℕ → Std.Format
      Instances For
        source
        @[instance_reducible]
        instance FloatLib.Numerics.instReprRationalInterval :
        Repr RationalInterval
        source
        def FloatLib.Numerics.RationalInterval.point (x : ℚ) :
        RationalInterval

        The degenerate interval containing one rational value.

        Instances For
          source
          def FloatLib.Numerics.RationalInterval.around (midpoint radius : ℚ) :
          RationalInterval

          An interval described by its midpoint and absolute-error radius.

          Instances For
            source
            def FloatLib.Numerics.RationalInterval.neg (interval : RationalInterval) :
            RationalInterval

            Negation reverses the endpoints.

            Instances For
              source
              def FloatLib.Numerics.RationalInterval.add (left right : RationalInterval) :
              RationalInterval

              Exact endpoint addition.

              Instances For
                source
                def FloatLib.Numerics.RationalInterval.sub (left right : RationalInterval) :
                RationalInterval

                Exact endpoint subtraction.

                Instances For
                  source
                  def FloatLib.Numerics.RationalInterval.scaleNonnegative (interval : RationalInterval) (factor : ℚ) :
                  RationalInterval

                  Multiply both endpoints by a nonnegative rational scale.

                  Instances For
                    source
                    def FloatLib.Numerics.RationalInterval.scale (interval : RationalInterval) (factor : ℚ) :
                    RationalInterval

                    Exact rational scaling, reversing the endpoints when the factor is negative.

                    Instances For
                      source
                      def FloatLib.Numerics.RationalInterval.squareNonnegative (interval : RationalInterval) :
                      RationalInterval

                      Square an interval known to contain a nonnegative value.

                      Clamping the lower endpoint at zero avoids squaring a negative error bound. This operation is used in exponential range reduction, where positivity follows from the function being enclosed.

                      Instances For
                        source
                        def FloatLib.Numerics.RationalInterval.squareRepeat (interval : RationalInterval) :
                        ℕ → RationalInterval

                        Repeated squaring of a nonnegative enclosure.

                        Instances For