OAI/Computability/LoopMatching/MachineMain.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. def OAI.LoopMatching.MachineMain.packBits line 13
  2. theorem OAI.LoopMatching.MachineMain.packBits_poly line 17
  3. lemma OAI.LoopMatching.MachineMain.packBits_value line 21
  4. lemma OAI.LoopMatching.MachineMain.packBits_length line 25
  5. def OAI.LoopMatching.MachineMain.serialize line 30
  6. theorem OAI.LoopMatching.MachineMain.serialize_poly line 32
  7. lemma OAI.LoopMatching.MachineMain.serialize_values line 36
  8. lemma OAI.LoopMatching.MachineMain.serialize_rawAccumulator line 40
  9. def OAI.LoopMatching.MachineMain.rawPair line 47
  10. theorem OAI.LoopMatching.MachineMain.rawPair_poly line 50
  11. def OAI.LoopMatching.MachineMain.runInput line 55
  12. theorem OAI.LoopMatching.MachineMain.runInput_poly line 57
  13. def OAI.LoopMatching.MachineMain.A line 61
  14. lemma OAI.LoopMatching.MachineMain.runInput_encoded line 65
  15. def OAI.LoopMatching.MachineMain.bitAlgorithm line 77
  16. theorem OAI.LoopMatching.MachineMain.bitAlgorithm_poly line 79
  17. def OAI.LoopMatching.MachineMain.binaryRoutine line 84
  18. lemma OAI.LoopMatching.MachineMain.bitAlgorithm_encoded line 87
  19. def OAI.LoopMatching.MachineMain.countingRoutine line 91
  20. theorem OAI.LoopMatching.MachineMain.computational_endpoint line 95