OAI/Combinatorics/EditApproximation/Queries/QueryReadBoundIrrelevance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Read budgets certify fixed buffer algorithms. Enlarging the budget changes proof arguments only, and preserves both values and work.

  1. theorem OAI.EditApproximation.BinaryFraction.queryGroupSelectWithWork_readBound_irrel line 19
  2. theorem OAI.EditApproximation.BinaryFraction.queryOnlineSelectWithWork_readBound_irrel line 28