OAI/Computability/LoopMatching/BitNormalize.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. def OAI.LoopMatching.BitNormalize.step line 12
  2. def OAI.LoopMatching.BitNormalize.normalize line 15
  3. lemma OAI.LoopMatching.BitNormalize.normalize_cons line 18
  4. lemma OAI.LoopMatching.BitNormalize.step_length line 21
  5. theorem OAI.LoopMatching.BitNormalize.length_normalize line 25
  6. lemma OAI.LoopMatching.BitNormalize.value_step line 34
  7. theorem OAI.LoopMatching.BitNormalize.value_normalize line 38
  8. theorem OAI.LoopMatching.BitNormalize.normalize_eq_bits line 43
  9. theorem OAI.LoopMatching.BitNormalize.normalize_bits line 65
  10. theorem OAI.LoopMatching.BitNormalize.normalize_idempotent line 68
  11. theorem OAI.LoopMatching.BitNormalize.step_poly line 71
  12. lemma OAI.LoopMatching.BitNormalize.step_growth line 75
  13. theorem OAI.LoopMatching.BitNormalize.normalize_poly line 83
  14. def OAI.LoopMatching.BitNormalize.add line 88
  15. theorem OAI.LoopMatching.BitNormalize.add_poly line 90
  16. theorem OAI.LoopMatching.BitNormalize.add_eq_bits line 92
  17. theorem OAI.LoopMatching.BitNormalize.value_add line 96
  18. theorem OAI.LoopMatching.BitNormalize.add_bits line 99
  19. theorem OAI.LoopMatching.BitNormalize.length_add line 102