OAI/Combinatorics/EditApproximation/Binary/BinaryRawStorage.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual Boolean word lengths in the materialized numerical implementation. These bounds use the stored unreduced values, without a gcd reduction.

  1. theorem OAI.EditApproximation.BinaryFraction.gradientCellWithWork_width line 12
  2. theorem OAI.EditApproximation.BinaryFraction.logarithmWithWork_width line 24
  3. theorem OAI.EditApproximation.BinaryFraction.dotListWithWork_width line 31
  4. theorem OAI.EditApproximation.BinaryFraction.finiteOptimizerWithWork_coordinate_normalized line 48
  5. theorem OAI.EditApproximation.BinaryFraction.finiteOptimizerWithWork_coordinate_width line 64