OAI/Combinatorics/EditApproximation/Queries/QueryRepresentatives.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Counted representative and child-coordinate lists for adaptive band data gathers. All initial-table lookups are included in the work counter.

  1. theorem OAI.EditApproximation.BinaryFraction.queryEarlierRepresentativesWithWork_value line 17
  2. theorem OAI.EditApproximation.BinaryFraction.queryWideInputsWithWork_value line 33
  3. theorem OAI.EditApproximation.BinaryFraction.queryBandInputsWithWork_value line 43