OAI/Computability/LoopMatching/RawAccumulator.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. abbrev OAI.LoopMatching.RawAccumulator.Data line 12
  2. abbrev OAI.LoopMatching.RawAccumulator.State line 13
  3. def OAI.LoopMatching.RawAccumulator.step line 15
  4. def OAI.LoopMatching.RawAccumulator.initial line 20
  5. def OAI.LoopMatching.RawAccumulator.rawAccumulator line 21
  6. def OAI.LoopMatching.RawAccumulator.term line 24
  7. theorem OAI.LoopMatching.RawAccumulator.step_poly line 26
  8. theorem OAI.LoopMatching.RawAccumulator.initial_poly line 30
  9. lemma OAI.LoopMatching.RawAccumulator.orbit_context line 34
  10. lemma OAI.LoopMatching.RawAccumulator.orbit_index line 39
  11. lemma OAI.LoopMatching.RawAccumulator.orbit_values line 44
  12. lemma OAI.LoopMatching.RawAccumulator.orbit_lengths line 54
  13. def OAI.LoopMatching.RawAccumulator.callBound line 76
  14. lemma OAI.LoopMatching.RawAccumulator.call_length_bound line 79
  15. lemma OAI.LoopMatching.RawAccumulator.state_code_length line 98
  16. def OAI.LoopMatching.RawAccumulator.orbitBound line 104
  17. lemma OAI.LoopMatching.RawAccumulator.orbit_bound line 106
  18. theorem OAI.LoopMatching.RawAccumulator.orbit_poly line 130
  19. theorem OAI.LoopMatching.RawAccumulator.rawAccumulator_poly line 134
  20. theorem OAI.LoopMatching.RawAccumulator.rawAccumulator_values line 138
  21. lemma OAI.LoopMatching.RawAccumulator.term_repr line 142
  22. theorem OAI.LoopMatching.RawAccumulator.rawAccumulator_repr line 147