OAI/Computability/LoopMatching/InputMachine.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. abbrev OAI.LoopMatching.InputMachine.LoopData line 11
  2. abbrev OAI.LoopMatching.InputMachine.Data line 12
  3. def OAI.LoopMatching.InputMachine.loopRepr line 14
  4. def OAI.LoopMatching.InputMachine.repr line 15
  5. def OAI.LoopMatching.InputMachine.crossBlock line 18
  6. def OAI.LoopMatching.InputMachine.cross line 21
  7. def OAI.LoopMatching.InputMachine.expanded line 24
  8. theorem OAI.LoopMatching.InputMachine.crossBlock_poly line 27
  9. theorem OAI.LoopMatching.InputMachine.cross_poly line 33
  10. theorem OAI.LoopMatching.InputMachine.expanded_poly line 41
  11. lemma OAI.LoopMatching.InputMachine.cross_repr line 47
  12. lemma OAI.LoopMatching.InputMachine.expanded_repr line 57
  13. def OAI.LoopMatching.InputMachine.call line 61
  14. theorem OAI.LoopMatching.InputMachine.call_poly line 63
  15. lemma OAI.LoopMatching.InputMachine.solve_repr line 66
  16. lemma OAI.LoopMatching.InputMachine.call_repr line 75