OAI/Combinatorics/EditApproximation/Binary/UnreducedOptimizer.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

A fraction-only implementation of the actual finite optimizer. None of its arithmetic or score comparisons requires reduced rational numbers.

  1. def OAI.EditApproximation.UnreducedRational.scoredArgmax line 15
  2. theorem OAI.EditApproximation.UnreducedRational.scoredArgmax_spec line 23
  3. def OAI.EditApproximation.UnreducedRational.dotList line 34
  4. def OAI.EditApproximation.UnreducedRational.dot line 38
  5. theorem OAI.EditApproximation.UnreducedRational.dotList_value line 41
  6. theorem OAI.EditApproximation.UnreducedRational.dot_value line 48
  7. def OAI.EditApproximation.UnreducedRational.gradientCell line 53
  8. def OAI.EditApproximation.UnreducedRational.gradient line 56
  9. theorem OAI.EditApproximation.UnreducedRational.gradient_value line 59
  10. def OAI.EditApproximation.UnreducedRational.maximizer line 64
  11. theorem OAI.EditApproximation.UnreducedRational.maximizer_value line 68
  12. def OAI.EditApproximation.UnreducedRational.finiteOptimizer line 82
  13. theorem OAI.EditApproximation.UnreducedRational.finiteOptimizer_value line 91
  14. theorem OAI.EditApproximation.UnreducedRational.maximizer_mem line 117
  15. theorem OAI.EditApproximation.UnreducedRational.finiteOptimizer_eq_iterate line 128
  16. theorem OAI.EditApproximation.UnreducedRational.finiteOptimizer_den_bits line 137
  17. theorem OAI.EditApproximation.UnreducedRational.finiteOptimizer_storageBits line 152