OAI/Computability/LoopMatching/InputDecode.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. abbrev OAI.LoopMatching.InputMachine.LoopBits line 10
  2. abbrev OAI.LoopMatching.InputMachine.BitsData line 11
  3. def OAI.LoopMatching.InputMachine.loopBitsRepr line 13
  4. def OAI.LoopMatching.InputMachine.bitsRepr line 14
  5. def OAI.LoopMatching.InputMachine.supportBound line 17
  6. def OAI.LoopMatching.InputMachine.decodeLoop line 19
  7. def OAI.LoopMatching.InputMachine.decode line 21
  8. theorem OAI.LoopMatching.InputMachine.decodeLoop_poly line 26
  9. theorem OAI.LoopMatching.InputMachine.decode_poly line 30
  10. lemma OAI.LoopMatching.InputMachine.supportBound_repr line 42
  11. lemma OAI.LoopMatching.InputMachine.decode_n_repr line 46
  12. lemma OAI.LoopMatching.InputMachine.decode_lengths line 50
  13. lemma OAI.LoopMatching.InputMachine.decode_repr line 54
  14. lemma OAI.LoopMatching.InputMachine.sparse_guard_repr line 81