ComparisonAccounting.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Accuracy accounting on the comparison tree

The clipped regrets cancel across every physical frontier. Terminal nodes can be carried forward in one child slot, with zero in the others, as in the complete-tree representation used for the curvature accounting.

theorem OAI.EditApproximation.tree_regret_telescope line 17
theorem OAI.EditApproximation.tree_regret_time_bound line 32

theorem OAI.EditApproximation.root_excess_from_time_bound line 54

Source documentation

Dividing the time telescope yields the positive-excess estimate. For clipped root values, root-D is exactly the positive part of error.

theorem root_excess_from_time_bound {S root D terminal charge regret error : ℝ}
    (hS : 0 < S)
    (htime : S * root ≤ S * (terminal + charge) + regret)
    (hterminal : terminal + charge ≤ D + error * D)
    (hregret : regret ≤ S * error * D) :
    root - D ≤ 2 * error * D := by
…