OAI/Combinatorics/EditApproximation/Binary/BinaryGradientWork.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A bit-operation bound for each actually materialized gradient coordinate.

  1. def OAI.EditApproximation.BinaryFraction.smoothingStorageBudget line 10
  2. def OAI.EditApproximation.BinaryFraction.shiftedStorageBudget line 12
  3. def OAI.EditApproximation.BinaryFraction.gradientLogStorageBudget line 14
  4. def OAI.EditApproximation.BinaryFraction.gradientCellBitBudget line 17
  5. theorem OAI.EditApproximation.BinaryFraction.gradientCellWithWork_cost line 25
  6. theorem OAI.EditApproximation.BinaryFraction.gradientCellBitBudget_mono line 93
  7. theorem OAI.EditApproximation.BinaryFraction.vectorMapWithWork_cost_le line 112
  8. theorem OAI.EditApproximation.BinaryFraction.gradientWithWork_cost line 123