OAI/Combinatorics/EditApproximation/Binary/BinaryRawOptimizer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Complete materialized entropy optimizer on Boolean fraction storage. Every arithmetic operation invokes the counted Boolean implementation.

  1. theorem OAI.EditApproximation.BinaryFraction.gradientWithWork_representation line 17
  2. theorem OAI.EditApproximation.BinaryFraction.scoredArgmaxWithWork_value line 31
  3. theorem OAI.EditApproximation.BinaryFraction.maximizerWithWork_representation line 44
  4. theorem OAI.EditApproximation.BinaryFraction.optimizerUpdateWithWork_representation line 67
  5. theorem OAI.EditApproximation.BinaryFraction.finiteOptimizerWithWork_representation line 80
  6. theorem OAI.EditApproximation.BinaryFraction.finiteOptimizerWithWork_value line 113