OAI/Combinatorics/MatchingEntropy/Face.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.LooplessGraph.positiveExtension line 16
  2. theorem OAI.MatchingEntropyBounds.LooplessGraph.positiveExtension_pos line 24
  3. theorem OAI.MatchingEntropyBounds.LooplessGraph.positiveExtension_zero line 29
  4. def OAI.MatchingEntropyBounds.LooplessGraph.degreeLinear line 33
  5. def OAI.MatchingEntropyBounds.LooplessGraph.cutLinear line 47
  6. def OAI.MatchingEntropyBounds.LooplessGraph.faceSpace line 52
  7. def OAI.MatchingEntropyBounds.LooplessGraph.faceCodimension line 67
  8. theorem OAI.MatchingEntropyBounds.LooplessGraph.faceCodimension_no_tight line 71
  9. theorem OAI.MatchingEntropyBounds.LooplessGraph.faceSpace_eventually_line line 85
  10. theorem OAI.MatchingEntropyBounds.LooplessGraph.faceSpace_of_eventually_line line 92
  11. abbrev OAI.MatchingEntropyBounds.LooplessGraph.sideMarginal line 119
  12. def OAI.MatchingEntropyBounds.LooplessGraph.sideRestriction line 122
  13. theorem OAI.MatchingEntropyBounds.LooplessGraph.positiveExtension_side line 129
  14. theorem OAI.MatchingEntropyBounds.LooplessGraph.sideMarginal_line line 136
  15. theorem OAI.MatchingEntropyBounds.LooplessGraph.faceSpace_of_side_spaces line 142
  16. theorem OAI.MatchingEntropyBounds.LooplessGraph.faceCodimension_le_sides line 171
  17. theorem OAI.MatchingEntropyBounds.LooplessGraph.faceCodimension_strong_aux line 182
  18. theorem OAI.MatchingEntropyBounds.LooplessGraph.faceCodimension_bound line 226
  19. theorem OAI.MatchingEntropyBounds.LooplessGraph.degree_add_smul line 241
  20. theorem OAI.MatchingEntropyBounds.LooplessGraph.cutMass_add_smul line 246
  21. theorem OAI.MatchingEntropyBounds.LooplessGraph.constraint_eventually_expand line 252
  22. theorem OAI.MatchingEntropyBounds.LooplessGraph.polytope_eventually_expand line 289