OAI/Combinatorics/EditApproximation/Binary/BinaryOnlineReads.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Online objective construction charges every historical table read, including repeated uses in gain and decrement terms.

  1. theorem OAI.EditApproximation.BinaryFraction.gainReadWithWork_eq line 17
  2. theorem OAI.EditApproximation.BinaryFraction.decrementReadWithWork_eq line 21
  3. theorem OAI.EditApproximation.BinaryFraction.optimisticTermReadWithWork_eq line 27
  4. theorem OAI.EditApproximation.BinaryFraction.optimisticTermReadWithWork_cost line 33
  5. theorem OAI.EditApproximation.BinaryFraction.onlineLinearReadWithWork_eq_cost line 44
  6. def OAI.EditApproximation.BinaryFraction.preparedBandOptimizerReadWithWork line 64
  7. theorem OAI.EditApproximation.BinaryFraction.preparedBandOptimizerReadWithWork_eq_cost line 74