OAI/Combinatorics/EditApproximation/Queries/QueryLocalSourcesCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complete random-source stage: source enumeration and range construction, physical source reads, finite-buffer scans, and the inner local refinement.

  1. def OAI.EditApproximation.BinaryFraction.queryLocalSourcesBitBudget line 13
  2. theorem OAI.EditApproximation.queryLocalRandomSources_work_bound line 40