OAI/Combinatorics/EditApproximation/Coarse/CoarseWidthWork.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The direct long-target branch removes dependence of initial-entry work on the target interval width. This is the source-width charge used when coarse leaves are summed over the physical dependency tree.

  1. theorem OAI.EditApproximation.coarseInitialArrayWork_expected_source_width line 13