OAI/Combinatorics/EditApproximation/Queries/QueryWideBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Band-buffer input construction has a polynomial counter in the number of representatives, emitted child-grid cells and key width.

  1. theorem OAI.EditApproximation.BinaryFraction.queryWideInputsWithWork_bounds line 21