OAI/Combinatorics/MatchingEntropy/EightVertex.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.Refined.obstructionGraph line 14
  2. def OAI.MatchingEntropyBounds.Refined.obstructionEdges line 19
  3. def OAI.MatchingEntropyBounds.Refined.obstructionUniform line 22
  4. def OAI.MatchingEntropyBounds.Refined.obstructionLaw line 24
  5. theorem OAI.MatchingEntropyBounds.Refined.obstruction_simple line 27
  6. theorem OAI.MatchingEntropyBounds.Refined.obstruction_matching line 31
  7. def OAI.MatchingEntropyBounds.Refined.obstructionMatching line 35
  8. theorem OAI.MatchingEntropyBounds.Refined.obstructionEdges_injective line 37
  9. theorem OAI.MatchingEntropyBounds.Refined.obstructionMatching_injective line 41
  10. theorem OAI.MatchingEntropyBounds.Refined.obstruction_binary_classify line 45
  11. theorem OAI.MatchingEntropyBounds.Refined.obstruction_classify line 63
  12. def OAI.MatchingEntropyBounds.Refined.obstructionEquiv line 106
  13. def OAI.MatchingEntropyBounds.Refined.obstructionSelected line 110
  14. theorem OAI.MatchingEntropyBounds.Refined.obstructionSelected_injective line 113
  15. theorem OAI.MatchingEntropyBounds.Refined.obstruction_law_eq_fiber line 117
  16. theorem OAI.MatchingEntropyBounds.Refined.obstruction_law_mean line 128
  17. theorem OAI.MatchingEntropyBounds.Refined.obstruction_law_feasible line 134
  18. theorem OAI.MatchingEntropyBounds.Refined.obstruction_uniform_mem line 139
  19. theorem OAI.MatchingEntropyBounds.Refined.obstruction_mean_coordinates line 142
  20. theorem OAI.MatchingEntropyBounds.Refined.obstruction_law_values line 159
  21. theorem OAI.MatchingEntropyBounds.Refined.obstruction_unique_law line 163
  22. theorem OAI.MatchingEntropyBounds.Refined.obstruction_entropy_law line 192
  23. theorem OAI.MatchingEntropyBounds.Refined.obstruction_maxEntropy line 196
  24. theorem OAI.MatchingEntropyBounds.Refined.obstruction_entropy_terms line 201
  25. theorem OAI.MatchingEntropyBounds.Refined.obstruction_logarithms line 217
  26. theorem OAI.MatchingEntropyBounds.Refined.eight_vertex_obstruction line 234