OAI/Combinatorics/EditApproximation/Binary/BinaryLocalOnlineReads.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Query-local online scales explicitly read the initial value at the query and at each rounded center before running the full band kernel.

  1. def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleReadWithWork line 22
  2. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleReadWithWork_eq line 36
  3. def OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsReadWithWork line 50
  4. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsReadWithWork_eq line 60