Error of repeatedly rounded reductions

The main bound adds the local absolute errors at the nodes actually visited by a reduction. It applies to any carrier with a real interpretation, so an executable floating-point tree does not first need to be replaced by a globally defined real rounding function.

mixedBudget propagates relative and absolute local errors through the schedule. The absolute term can cover gradual underflow; setting it to zero gives a relative-error specialization. These are round-per-node bounds, not bounds for an exact accumulator rounded only at the end.

noncomputable def FloatLib.Numerics.ReductionTree.errorBudget {α : Type u_1} {β : Type u_2} (combine : β → β → β) (value : α → β) (allowance : β → β → ℝ) : ReductionTree α → ℝ

Sum of local error allowances, evaluated at the actual operands of each internal node.

theorem FloatLib.Numerics.ReductionTree.abs_eval_sub_exact_le_errorBudget {α : Type u_1} {β : Type u_2} (t : ReductionTree α) (combine : β → β → β) (value : α → β) (interpret : β → ℝ) (allowance : β → β → ℝ) (h : AllNodes combine value (fun (x y : β) => |interpret (combine x y) - (interpret x + interpret y)| ≤ allowance x y) t) : |interpret (eval combine value t) - eval (fun (x1 x2 : ℝ) => x1 + x2) (interpret ∘ value) t| ≤ errorBudget combine value allowance t

Local bounds are required only for pairs of operands encountered in this schedule.

theorem FloatLib.Numerics.ReductionTree.errorBudget_const {α : Type u_1} {β : Type u_2} (t : ReductionTree α) (combine : β → β → β) (value : α → β) (δ : ℝ) : errorBudget combine value (fun (x x_1 : β) => δ) t = ↑t.nodeCount * δ

A uniform absolute allowance is paid once per addition, independently of tree shape.

theorem FloatLib.Numerics.ReductionTree.abs_eval_sub_exact_le_nodeCount {α : Type u_1} {β : Type u_2} (t : ReductionTree α) (combine : β → β → β) (value : α → β) (interpret : β → ℝ) (δ : ℝ) (h : AllNodes combine value (fun (x y : β) => |interpret (combine x y) - (interpret x + interpret y)| ≤ δ) t) : |interpret (eval combine value t) - eval (fun (x1 x2 : ℝ) => x1 + x2) (interpret ∘ value) t| ≤ ↑t.nodeCount * δ

Absolute local error alone suffices, including near zero.

noncomputable def FloatLib.Numerics.ReductionTree.mixedBudget {α : Type u_1} (value : α → ℝ) (u δ : ℝ) : ReductionTree α → ℝ

A priori mixed error bound using exact subtree sums, not rounded intermediate values.

theorem FloatLib.Numerics.ReductionTree.abs_eval_sub_exact_le_mixedBudget {α : Type u_1} {β : Type u_2} (t : ReductionTree α) (combine : β → β → β) (value : α → β) (interpret : β → ℝ) (u δ : ℝ) (hu : 0 ≤ u) (h : AllNodes combine value (fun (x y : β) => |interpret (combine x y) - (interpret x + interpret y)| ≤ u * (|interpret x| + |interpret y|) + δ) t) : |interpret (eval combine value t) - eval (fun (x1 x2 : ℝ) => x1 + x2) (interpret ∘ value) t| ≤ mixedBudget (interpret ∘ value) u δ t

Propagate a mixed relative/absolute bound through the actual reduction schedule.

theorem FloatLib.Numerics.ReductionTree.abs_eval_sub_exact_le_relativeBudget {α : Type u_1} {β : Type u_2} (t : ReductionTree α) (combine : β → β → β) (value : α → β) (interpret : β → ℝ) (u : ℝ) (hu : 0 ≤ u) (h : AllNodes combine value (fun (x y : β) => |interpret (combine x y) - (interpret x + interpret y)| ≤ u * (|interpret x| + |interpret y|)) t) : |interpret (eval combine value t) - eval (fun (x1 x2 : ℝ) => x1 + x2) (interpret ∘ value) t| ≤ mixedBudget (interpret ∘ value) u 0 t

Relative-only analysis is the mixed bound with zero absolute allowance.

noncomputable def FloatLib.Numerics.ReductionTree.sumAbs {α : Type u_1} (value : α → ℝ) (t : ReductionTree α) : ℝ

The absolute-input scale of a reduction, invariant under reordering.

theorem FloatLib.Numerics.ReductionTree.sumAbs_nonneg {α : Type u_1} (value : α → ℝ) (t : ReductionTree α) : 0 ≤ sumAbs value t

The absolute-input scale is nonnegative, even for a sum that cancels exactly.

theorem FloatLib.Numerics.ReductionTree.sumAbs_eq_of_perm {α : Type u_1} {a b : ReductionTree α} (h : a.leaves.Perm b.leaves) (value : α → ℝ) : sumAbs value a = sumAbs value b

Reordering does not change the absolute-input scale of the common enclosure.

theorem FloatLib.Numerics.ReductionTree.abs_eval_add_le_sumAbs {α : Type u_1} (value : α → ℝ) (t : ReductionTree α) : |eval (fun (x1 x2 : ℝ) => x1 + x2) value t| ≤ sumAbs value t

Cancellation can reduce the exact sum but not its absolute-input scale.

theorem FloatLib.Numerics.ReductionTree.mixedBudget_zero_le {α : Type u_1} (value : α → ℝ) (u : ℝ) (hu : 0 ≤ u) (t : ReductionTree α) : mixedBudget value u 0 t ≤ ((1 + u) ^ t.nodeCount - 1) * sumAbs value t

A relative-only budget is bounded uniformly over all schedules of the same size and scale.

theorem FloatLib.Numerics.ReductionTree.abs_eval_sub_exact_le_geometric {α : Type u_1} {β : Type u_2} (t : ReductionTree α) (combine : β → β → β) (value : α → β) (interpret : β → ℝ) (u : ℝ) (hu : 0 ≤ u) (h : AllNodes combine value (fun (x y : β) => |interpret (combine x y) - (interpret x + interpret y)| ≤ u * (|interpret x| + |interpret y|)) t) : |interpret (eval combine value t) - eval (fun (x1 x2 : ℝ) => x1 + x2) (interpret ∘ value) t| ≤ ((1 + u) ^ t.nodeCount - 1) * sumAbs (interpret ∘ value) t

The familiar geometric enclosure depends only on leaf count and absolute-input scale. The relative premise is still local to this tree; no global floating-point relative bound is assumed. nodeCount = leaves.length - 1 by length_leaves.

theorem FloatLib.Numerics.ReductionTree.abs_eval_sub_eval_le_geometric {α : Type u_1} {β : Type u_2} {a b : ReductionTree α} (combine : β → β → β) (value : α → β) (interpret : β → ℝ) (u : ℝ) (hu : 0 ≤ u) (hperm : a.leaves.Perm b.leaves) (ha : AllNodes combine value (fun (x y : β) => |interpret (combine x y) - (interpret x + interpret y)| ≤ u * (|interpret x| + |interpret y|)) a) (hb : AllNodes combine value (fun (x y : β) => |interpret (combine x y) - (interpret x + interpret y)| ≤ u * (|interpret x| + |interpret y|)) b) : |interpret (eval combine value a) - interpret (eval combine value b)| ≤ 2 * (((1 + u) ^ a.nodeCount - 1) * sumAbs (interpret ∘ value) a)

Two locally bounded schedules over the same multiset share the same geometric enclosure.