OAI/Combinatorics/EditApproximation/Binary/BinaryPreparedComputedCellWork.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The cell cost includes materializing the exact dyadic scale array; the finite draw counts are then those of the original cell sampler.

  1. theorem OAI.EditApproximation.BinaryFraction.preparedComputedCellGroupWithWork_cost line 13