OAI/Combinatorics/MatchingEntropy/Polytope.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.LooplessGraph.supportSimple line 16
  2. theorem OAI.MatchingEntropyBounds.LooplessGraph.supportSimple_edge line 24
  3. theorem OAI.MatchingEntropyBounds.LooplessGraph.sum_pred_le_one line 27
  4. theorem OAI.MatchingEntropyBounds.LooplessGraph.odd_family_bound line 43
  5. theorem OAI.MatchingEntropyBounds.LooplessGraph.supportSimple_has_perfectMatching line 131
  6. theorem OAI.MatchingEntropyBounds.LooplessGraph.exists_supported_matching line 186
  7. theorem OAI.MatchingEntropyBounds.LooplessGraph.crosses_singleton line 231
  8. theorem OAI.MatchingEntropyBounds.LooplessGraph.cutMass_singleton line 239
  9. theorem OAI.MatchingEntropyBounds.LooplessGraph.constraint_eventually_line line 245
  10. theorem OAI.MatchingEntropyBounds.LooplessGraph.degree_sub line 284
  11. theorem OAI.MatchingEntropyBounds.LooplessGraph.cutMass_sub line 290
  12. theorem OAI.MatchingEntropyBounds.LooplessGraph.trivial_tight_cut_preserved line 297
  13. theorem OAI.MatchingEntropyBounds.LooplessGraph.extreme_no_tight_integral line 316
  14. theorem OAI.MatchingEntropyBounds.LooplessGraph.constraint_subset_polytope_aux line 334
  15. theorem OAI.MatchingEntropyBounds.LooplessGraph.polytope_eq_constraints line 372