OAI/Combinatorics/MatchingCount/Algorithm/TreeWeights.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableSource.PathData line 10
  2. def OAI.MatchingFPRAS.ExecutableSource.path line 12
  3. def OAI.MatchingFPRAS.ExecutableSource.pathRealizer line 15
  4. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_path line 21
  5. lemma OAI.MatchingFPRAS.ExecutableSource.path_repr line 30
  6. def OAI.MatchingFPRAS.ExecutableSource.vertexEqual line 54
  7. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_vertexEqual line 56
  8. def OAI.MatchingFPRAS.ExecutableSource.sameEnds line 60
  9. def OAI.MatchingFPRAS.ExecutableSource.sameEndsRealizer line 62
  10. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sameEnds line 69
  11. lemma OAI.MatchingFPRAS.ExecutableSource.sameEnds_sym2 line 75
  12. abbrev OAI.MatchingFPRAS.ExecutableSource.WeightedEdge line 78
  13. abbrev OAI.MatchingFPRAS.ExecutableSource.PathTableInput line 79
  14. def OAI.MatchingFPRAS.ExecutableSource.pathRow line 81
  15. def OAI.MatchingFPRAS.ExecutableSource.pathRowRealizer line 83
  16. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_pathRow line 87
  17. def OAI.MatchingFPRAS.ExecutableSource.pathTable line 96
  18. def OAI.MatchingFPRAS.ExecutableSource.pathTableRealizer line 98
  19. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_pathTable line 100
  20. def OAI.MatchingFPRAS.ExecutableSource.contribution line 108
  21. def OAI.MatchingFPRAS.ExecutableSource.contributionRealizer line 110
  22. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_contribution line 112
  23. def OAI.MatchingFPRAS.ExecutableSource.activity line 119
  24. def OAI.MatchingFPRAS.ExecutableSource.activityRealizer line 121
  25. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_activity line 123