OAI/Computability/LoopMatching/BinaryMultiply.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. abbrev OAI.LoopMatching.SmallBinaryMultiply.State line 10
  2. def OAI.LoopMatching.SmallBinaryMultiply.step line 12
  3. def OAI.LoopMatching.SmallBinaryMultiply.initial line 13
  4. def OAI.LoopMatching.SmallBinaryMultiply.mul line 14
  5. theorem OAI.LoopMatching.SmallBinaryMultiply.step_poly line 16
  6. theorem OAI.LoopMatching.SmallBinaryMultiply.initial_poly line 20
  7. lemma OAI.LoopMatching.SmallBinaryMultiply.orbit_first line 24
  8. lemma OAI.LoopMatching.SmallBinaryMultiply.orbit_value line 30
  9. lemma OAI.LoopMatching.SmallBinaryMultiply.orbit_length line 39
  10. lemma OAI.LoopMatching.SmallBinaryMultiply.orbit_code_length line 57
  11. theorem OAI.LoopMatching.SmallBinaryMultiply.orbit_poly line 64
  12. theorem OAI.LoopMatching.SmallBinaryMultiply.mul_poly line 81
  13. theorem OAI.LoopMatching.SmallBinaryMultiply.value_mul line 85
  14. theorem OAI.LoopMatching.SmallBinaryMultiply.length_mul line 88
  15. def OAI.LoopMatching.SmallBinaryMultiply.horner line 91
  16. theorem OAI.LoopMatching.SmallBinaryMultiply.horner_poly line 94
  17. theorem OAI.LoopMatching.SmallBinaryMultiply.value_horner line 98
  18. theorem OAI.LoopMatching.SmallBinaryMultiply.length_horner line 102