TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Automation.Interval.Aggregates

Finite aggregates for interval reification #

Concrete finite sums and norms are expanded into scalar arithmetic with equality certificates. Splitting Fin and range sums in halves keeps the resulting additions balanced.

source
theorem FloatLib.Numerics.Interval.Tactic.sup_univ_fin_add {a b : ℕ} (f : Fin (a + b) → NNReal) :
Finset.univ.sup f = max (Finset.univ.sup fun (i : Fin a) => f (Fin.castAdd b i)) (Finset.univ.sup fun (i : Fin b) => f (Fin.natAdd a i))

Split a finite supremum along the two consecutive blocks of a Fin index.

source
def FloatLib.Numerics.Interval.Tactic.aggregateEquality (proof : Lean.Expr) :
Lean.MetaM Lean.Meta.Simp.Result

Turn an equality into a simplifier result without normalizing either side.

Instances For
    source
    def FloatLib.Numerics.Interval.Tactic.expandAggregateSum (e : Lean.Expr) :
    Lean.MetaM (Option Lean.Meta.Simp.Result)

    Expand one finite real sum, using balanced partitions for numerical dimensions.

    Instances For
      source
      def FloatLib.Numerics.Interval.Tactic.expandAggregateSup (e : Lean.Expr) :
      Lean.MetaM (Option Lean.Meta.Simp.Result)

      Expand a nonnegative finite supremum; coercions then expose real maxima.

      Instances For
        source
        def FloatLib.Numerics.Interval.Tactic.aggregateNat :
        Lean.Meta.Simp.Simproc

        Reduce closed natural coefficients, including projections of generated Fin indices.

        Instances For
          source
          def FloatLib.Numerics.Interval.Tactic.aggregatePre :
          Lean.Meta.Simp.Simproc

          The aggregate expansion is local to the interval tactic.

          Instances For
            source
            def FloatLib.Numerics.Interval.Tactic.aggregateAtoms :
            Lean.Meta.Simp.Simproc

            Keep unsupported real functions intact instead of simplifying inside their arguments.

            Instances For
              source
              def FloatLib.Numerics.Interval.Tactic.decideAggregateGuard? (p : Lean.Expr) :
              Lean.MetaM (Option Lean.Expr)

              Prove a closed guard only after its decision procedure reduces to true.

              Instances For
                source
                def FloatLib.Numerics.Interval.Tactic.aggregateScalarTheorems :
                Lean.MetaM Lean.Meta.SimpTheorems

                Scalar coercions preserve arithmetic; truncated subtraction becomes a maximum.

                Instances For
                  source
                  def FloatLib.Numerics.Interval.Tactic.normalizeAggregateNumerals (e : Q(ℝ)) :
                  Lean.MetaM Lean.Meta.Simp.Result

                  Expose numerical coefficients without expanding aggregates or evaluating real arithmetic.

                  Instances For
                    source
                    def FloatLib.Numerics.Interval.Tactic.normalizeAggregates (e : Q(ℝ)) :
                    Lean.MetaM Lean.Meta.Simp.Result

                    Normalize concrete finite sums, dot products, matrix entries, and l1/infinity norms.

                    The result contains the scalar expression and a proof of equality to the input. A caller proving reification correctness can compose this proof with a structural proof for the normalized scalar expression, without running arithmetic simplification on the expanded aggregate.

                    Instances For