TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Enclosure.Expression.Check

Checking real inequalities on rational boxes #

Expr.check evaluates an interval expression and checks its decoded upper bound against zero. An inconclusive evaluation can subdivide the widest positive-width input interval at its exact rational midpoint. Both children must succeed. Precision and elementary-function approximation settings belong to the backend; the checker controls only the subdivision depth.

Input coordinates have explicit rational bounds. A missing variable, failed endpoint conversion, or rejected operation makes a leaf fail. CheckProof proves that successful checks establish the inequality for every real assignment in the original box.

source
@[reducible, inline]
abbrev FloatLib.Numerics.Interval.Box :
Type

Rational bounds for variables numbered from zero.

Instances For
    source
    inductive FloatLib.Numerics.Interval.Relation :
    Type

    Whether the expression must be nonpositive or strictly negative throughout the box.

    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Numerics.Interval.instDecidableEqRelation :
      DecidableEq Relation
      source
      @[instance_reducible]
      instance FloatLib.Numerics.Interval.instReprRelation :
      Repr Relation
      source
      def FloatLib.Numerics.Interval.instReprRelation.repr :
      Relation → ℕ → Std.Format
      Instances For
        source
        def FloatLib.Numerics.Interval.Relation.check (relation : Relation) (hi : ℚ) :
        Bool

        Test a rational upper bound against zero.

        Instances For
          source
          def FloatLib.Numerics.Interval.Backend.encloseInterval? {α : Type u_1} (B : Backend α) (I : Interval ℚ) :
          Option (Interval α)

          Enclose both rational endpoints and keep the outward-facing bounds.

          Instances For
            source
            def FloatLib.Numerics.Interval.Box.enclose? {α : Type u_1} (box : Box) (B : Backend α) :
            Option (List (Interval α))

            Enclose every coordinate, failing if either endpoint of any coordinate cannot be enclosed.

            Instances For
              source
              def FloatLib.Numerics.Interval.Box.widest? (box : Box) :
              Option (ℕ × ℚ)

              Index and width of the widest positive-width coordinate; ties choose the first coordinate.

              Instances For
                source
                def FloatLib.Numerics.Interval.Box.bisect? (box : Box) :
                Option (Box × Box)

                Bisect the widest positive-width coordinate at its exact rational midpoint.

                The two closed children share the midpoint and cover the original box.

                Instances For
                  source
                  def FloatLib.Numerics.Interval.Expr.checkBox {α : Type u_1} (e : Expr) (B : Backend α) (relation : Relation) (box : Box) :
                  Bool

                  Check one box using the decoded upper endpoint of a successful expression evaluation.

                  Instances For
                    source
                    def FloatLib.Numerics.Interval.Expr.check {α : Type u_1} (e : Expr) (B : Backend α) (relation : Relation) (box : Box) (depth : ℕ) :
                    Bool

                    Check a real inequality, subdividing inconclusive boxes up to the supplied depth.

                    Depth zero performs a single interval evaluation. A split succeeds only when both children succeed, including when the original evaluation rejected an operation's domain.

                    Instances For