OAI/Combinatorics/MatchingCount/Sampling/TreeClippedDP.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutableDP.nVertices line 11
  2. def OAI.MatchingFPRAS.ExecutableDP.nLabels line 12
  3. def OAI.MatchingFPRAS.ExecutableDP.nPlan line 13
  4. def OAI.MatchingFPRAS.ExecutableDP.BInitial line 14
  5. def OAI.MatchingFPRAS.ExecutableDP.capBits line 15
  6. def OAI.MatchingFPRAS.ExecutableDP.nVerticesRealizer line 17
  7. def OAI.MatchingFPRAS.ExecutableDP.nLabelsRealizer line 18
  8. def OAI.MatchingFPRAS.ExecutableDP.nPlanRealizer line 19
  9. def OAI.MatchingFPRAS.ExecutableDP.BInitialRealizer line 20
  10. def OAI.MatchingFPRAS.ExecutableDP.capBitsRealizer line 21
  11. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_nVertices line 27
  12. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_nLabels line 28
  13. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_nPlan line 29
  14. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_BInitial line 30
  15. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_capBits line 32
  16. lemma OAI.MatchingFPRAS.ExecutableDP.input_lengths line 43
  17. lemma OAI.MatchingFPRAS.ExecutableDP.BInitial_bound line 47
  18. lemma OAI.MatchingFPRAS.ExecutableDP.capBits_bound line 50
  19. def OAI.MatchingFPRAS.ExecutableDP.initialEntry line 59
  20. def OAI.MatchingFPRAS.ExecutableDP.initialEntryRealizer line 60
  21. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_initialEntry line 62
  22. def OAI.MatchingFPRAS.ExecutableDP.initialFast line 70
  23. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_initialFast line 80
  24. abbrev OAI.MatchingFPRAS.ExecutableDP.UpdateInput line 86
  25. def OAI.MatchingFPRAS.ExecutableDP.updateRows line 87
  26. def OAI.MatchingFPRAS.ExecutableDP.updateColumns line 88
  27. def OAI.MatchingFPRAS.ExecutableDP.updateRowsRealizer line 89
  28. def OAI.MatchingFPRAS.ExecutableDP.updateColumnsRealizer line 90
  29. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_updateRows line 93
  30. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_updateColumns line 95
  31. lemma OAI.MatchingFPRAS.ExecutableDP.update_dimensions line 101
  32. def OAI.MatchingFPRAS.ExecutableDP.cappedEntry line 107
  33. def OAI.MatchingFPRAS.ExecutableDP.cappedEntryRealizer line 108
  34. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_cappedEntry line 111
  35. def OAI.MatchingFPRAS.ExecutableDP.cappedUpdate line 121
  36. def OAI.MatchingFPRAS.ExecutableDP.cappedUpdateRealizer line 122
  37. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_cappedUpdate line 123