TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Reduction.Tree

Finite, repeatedly rounded binary sums #

Each internal node uses Model.add, with one nearest-even rounding at that node. A finite execution certificate excludes exceptional inputs and overflow at every intermediate result. The error budget then follows from FloatLib's half-ULP theorem, including subnormal values. This API does not change Model.sum, which accumulates exactly and rounds only once.

source
def FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.FiniteEval {fmt : FloatFormat} :
Numerics.ReductionTree (Model fmt) → Prop

All leaves and intermediate additions have real denotations.

Instances For
    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.FiniteEval.isFinite_eval {fmt : FloatFormat} {t : Numerics.ReductionTree (Model fmt)} (h : FiniteEval t) :
    (Numerics.ReductionTree.eval add id t).isFinite = true

    Finiteness of the root is part of a finite execution certificate.

    source
    theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.toReal_eval {fmt : FloatFormat} (t : Numerics.ReductionTree (Model fmt)) (hfmt : fmt.isIEEE = true) (hfinite : FiniteEval t) :
    (Numerics.ReductionTree.eval add id t).toReal = Numerics.ReductionTree.eval (fun (x y : ℝ) => roundAt fmt (x + y)) toReal t

    The rounded real interpretation agrees with encoded execution at each finite node.

    source
    noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.errorBudget {fmt : FloatFormat} (t : Numerics.ReductionTree (Model fmt)) :
    ℝ

    The sum of half-ULPs at the actual intermediate additions.

    Instances For
      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.abs_toReal_eval_sub_sum_le {fmt : FloatFormat} (t : Numerics.ReductionTree (Model fmt)) (hfmt : fmt.isIEEE = true) (hfinite : FiniteEval t) :
      |(Numerics.ReductionTree.eval add id t).toReal - (List.map toReal t.leaves).sum| ≤ errorBudget t

      No normal-range hypothesis is needed: each finite addition has an absolute half-ULP bound.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ReductionTree.abs_toReal_eval_sub_eval_le {fmt : FloatFormat} {a b : Numerics.ReductionTree (Model fmt)} (hfmt : fmt.isIEEE = true) (ha : FiniteEval a) (hb : FiniteEval b) (hperm : a.leaves.Perm b.leaves) :
      |(Numerics.ReductionTree.eval add id a).toReal - (Numerics.ReductionTree.eval add id b).toReal| ≤ errorBudget a + errorBudget b

      Two finite schedules over the same inputs can differ by at most their combined budgets.