OAI/Combinatorics/MatchingEntropy/OddCuts.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.LooplessGraph.Crosses line 16

    Also declared: ComparatorChallenges/TriangleFace.lean:59 (same declaration text).

  2. instance OAI.MatchingEntropyBounds.LooplessGraph.crossesDecidable line 19

    Also declared: ComparatorChallenges/TriangleFace.lean:62 (same declaration text).

  3. def OAI.MatchingEntropyBounds.LooplessGraph.cut line 23

    Also declared: ComparatorChallenges/TriangleFace.lean:66 (same declaration text).

  4. def OAI.MatchingEntropyBounds.LooplessGraph.degree line 26

    Also declared: ComparatorChallenges/TriangleFace.lean:69 (same declaration text).

  5. def OAI.MatchingEntropyBounds.LooplessGraph.cutMass line 29

    Also declared: ComparatorChallenges/TriangleFace.lean:72 (same declaration text).

  6. def OAI.MatchingEntropyBounds.LooplessGraph.constraintPolytope line 32
  7. theorem OAI.MatchingEntropyBounds.LooplessGraph.mem_cut line 37
  8. theorem OAI.MatchingEntropyBounds.LooplessGraph.crosses_compl line 41
  9. theorem OAI.MatchingEntropyBounds.LooplessGraph.cut_compl line 47
  10. theorem OAI.MatchingEntropyBounds.LooplessGraph.degree_indicator line 51
  11. theorem OAI.MatchingEntropyBounds.LooplessGraph.degree_mean line 66
  12. theorem OAI.MatchingEntropyBounds.LooplessGraph.incidence_sum line 83
  13. theorem OAI.MatchingEntropyBounds.LooplessGraph.matching_incidence_count line 98
  14. theorem OAI.MatchingEntropyBounds.LooplessGraph.matching_crosses_odd line 118
  15. theorem OAI.MatchingEntropyBounds.LooplessGraph.degree_linear line 136
  16. theorem OAI.MatchingEntropyBounds.LooplessGraph.cutMass_linear line 145
  17. theorem OAI.MatchingEntropyBounds.LooplessGraph.convex_constraintPolytope line 150
  18. theorem OAI.MatchingEntropyBounds.LooplessGraph.indicator_mem_constraintPolytope line 164
  19. theorem OAI.MatchingEntropyBounds.LooplessGraph.polytope_subset_constraintPolytope line 176
  20. theorem OAI.MatchingEntropyBounds.LooplessGraph.constraint_coordinate_le_one line 184
  21. theorem OAI.MatchingEntropyBounds.LooplessGraph.continuous_degree line 194
  22. theorem OAI.MatchingEntropyBounds.LooplessGraph.continuous_cutMass line 202
  23. theorem OAI.MatchingEntropyBounds.LooplessGraph.isClosed_constraintPolytope line 208
  24. theorem OAI.MatchingEntropyBounds.LooplessGraph.isCompact_constraintPolytope line 217