OAI/Combinatorics/EditApproximation/Queries/QueryOnlineRangeCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Online source ranges are computed before their random draws. This charges the actual band, coordinate set, two powers, and triangular mass.

  1. def OAI.EditApproximation.BinaryFraction.queryOnlineRangeBitBudget line 12
  2. theorem OAI.EditApproximation.BinaryFraction.queryOnlineRangeWithWork_bounds line 19