OAI/Combinatorics/EditApproximation/Binary/BinaryReadCostBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Lookup overhead is controlled by the loops that actually run. These comparisons require only a bound on one finite-buffer lookup.

  1. theorem OAI.EditApproximation.vectorMapWithWork_cost_lower line 14
  2. theorem OAI.EditApproximation.arithmeticMapWithWork_factor line 22
  3. theorem OAI.EditApproximation.vectorMapWithWork_factor line 40
  4. theorem OAI.EditApproximation.filterWithWork_factor line 60
  5. theorem OAI.EditApproximation.allWithWork_factor line 78
  6. theorem OAI.EditApproximation.filterMapWithWork_factor line 96
  7. theorem OAI.EditApproximation.cost_replace_factor line 116

    Source documentation

    Multiplicative work bounds are preserved when the same nonnegative overhead is added to both counters.

    theorem cost_replace_factor (a c old new K : ℕ) (hc : c ≤ a * K) (hK : 1 ≤ K)
    (ha : a ≤ old) (hn : new + a ≤ old + c) : new ≤ old * K := by
…
  8. theorem OAI.EditApproximation.cost_factor_with_read line 127

    Source documentation

    A compulsory constant instruction pays for one additional lookup.

    theorem cost_factor_with_read (a c x r R K : ℕ) (hc : c ≤ a * K)
    (hr : r ≤ R) (hx : 1 ≤ x) (hK : R + 1 ≤ K) :
    r + c + x ≤ (a + x) * K := by
…
  9. def OAI.EditApproximation.BinaryFraction.tableReadFactor line 141
  10. theorem OAI.EditApproximation.BinaryFraction.tableReadFactor_pos line 143
  11. theorem OAI.EditApproximation.BinaryFraction.tableReadFactor_absorb line 147
  12. theorem OAI.EditApproximation.BinaryFraction.endpointScoreReadWithWork_factor line 156
  13. theorem OAI.EditApproximation.BinaryFraction.prefixReadWithWork_factor line 165
  14. theorem OAI.EditApproximation.BinaryFraction.bandEnvelopeReadWithWork_factor line 183
  15. theorem OAI.EditApproximation.BinaryFraction.onlineLinearReadWithWork_factor line 192