OAI/Combinatorics/EditApproximation/Binary/BinaryOnlineReadCosts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Online sampler arithmetic and lookup costs share one linear read factor.

  1. theorem OAI.EditApproximation.BinaryFraction.countedPreparedActionReadWithWork_factor line 11
  2. theorem OAI.EditApproximation.BinaryFraction.countedBandActionReadWithWork_factor line 32
  3. theorem OAI.EditApproximation.BinaryFraction.countedSampledOnlineReadWithWork_factor line 53
  4. def OAI.EditApproximation.BinaryFraction.onlineCostCore line 70
  5. theorem OAI.EditApproximation.BinaryFraction.onlineCostCore_factor line 84
  6. theorem OAI.EditApproximation.BinaryFraction.preparedOnlineReadWithWork_factor line 115