OAI/Combinatorics/PerfectMatching/OddCuts.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Degree and odd-cut constraints for the perfect matching polytope.

  1. def OAI.MatchingEntropy.LooplessGraph.Crosses line 21

    Source documentation

    Exactly one endpoint in S; edge identities are kept, including parallels.

    def Crosses (G : LooplessGraph V E) (S : Finset V) (e : E) : Prop :=
…
  2. instance OAI.MatchingEntropy.LooplessGraph.crossesDecidable line 24
  3. def OAI.MatchingEntropy.LooplessGraph.cut line 28
  4. def OAI.MatchingEntropy.LooplessGraph.degree line 31
  5. def OAI.MatchingEntropy.LooplessGraph.cutMass line 34
  6. def OAI.MatchingEntropy.LooplessGraph.constraintPolytope line 38

    Source documentation

    The degree and odd-cut constraint system.

    def constraintPolytope (G : LooplessGraph V E) : Set (E → ℝ) :=
…
  7. theorem OAI.MatchingEntropy.LooplessGraph.mem_cut line 43
  8. theorem OAI.MatchingEntropy.LooplessGraph.crosses_compl line 47
  9. theorem OAI.MatchingEntropy.LooplessGraph.cut_compl line 53
  10. theorem OAI.MatchingEntropy.LooplessGraph.degree_indicator line 57
  11. theorem OAI.MatchingEntropy.LooplessGraph.degree_mean line 72
  12. theorem OAI.MatchingEntropy.LooplessGraph.incidence_sum line 89
  13. theorem OAI.MatchingEntropy.LooplessGraph.matching_incidence_count line 104
  14. theorem OAI.MatchingEntropy.LooplessGraph.matching_crosses_odd line 124
  15. theorem OAI.MatchingEntropy.LooplessGraph.degree_linear line 143
  16. theorem OAI.MatchingEntropy.LooplessGraph.cutMass_linear line 152
  17. theorem OAI.MatchingEntropy.LooplessGraph.convex_constraintPolytope line 157
  18. theorem OAI.MatchingEntropy.LooplessGraph.indicator_mem_constraintPolytope line 171
  19. theorem OAI.MatchingEntropy.LooplessGraph.polytope_subset_constraintPolytope line 183
  20. theorem OAI.MatchingEntropy.LooplessGraph.constraint_coordinate_le_one line 191
  21. theorem OAI.MatchingEntropy.LooplessGraph.continuous_degree line 201
  22. theorem OAI.MatchingEntropy.LooplessGraph.continuous_cutMass line 209
  23. theorem OAI.MatchingEntropy.LooplessGraph.isClosed_constraintPolytope line 215
  24. theorem OAI.MatchingEntropy.LooplessGraph.isCompact_constraintPolytope line 224