OAI/Combinatorics/EditApproximation/Binary/BinaryOuterReadCosts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The outer local loops preserve the same lookup factor, including initial-value reads at the query and at rounded representative centers.

  1. theorem OAI.EditApproximation.BinaryFraction.cost_replace_with_read line 15
  2. theorem OAI.EditApproximation.BinaryFraction.preparedComputedCellReadWithWork_factor line 34
  3. theorem OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleReadWithWork_factor line 50
  4. theorem OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsReadWithWork_factor line 77
  5. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineScaleReadWithWork_factor line 132
  6. theorem OAI.EditApproximation.BinaryFraction.preparedLocalOnlineActionsReadWithWork_factor line 154