OAI/Combinatorics/MatchingEntropy/KleeSharpness.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingEntropyBounds.Refined.colorMatching_indicator line 18
  2. theorem OAI.MatchingEntropyBounds.Refined.colorMatching_injective line 24
  3. theorem OAI.MatchingEntropyBounds.Refined.coloredVector_linearIndependent line 34
  4. theorem OAI.MatchingEntropyBounds.Refined.colored_uniform_mean line 44
  5. theorem OAI.MatchingEntropyBounds.Refined.expanded_colorMatching line 54
  6. theorem OAI.MatchingEntropyBounds.Refined.triangleExtension_colored line 68
  7. theorem OAI.MatchingEntropyBounds.Refined.kleeEDecEq_succ line 79
  8. theorem OAI.MatchingEntropyBounds.Refined.kleeVDecEq_succ line 80
  9. theorem OAI.MatchingEntropyBounds.Refined.kleeEDecEq_zero line 81
  10. theorem OAI.MatchingEntropyBounds.Refined.klee_law_eq_fiber line 83
  11. theorem OAI.MatchingEntropyBounds.Refined.klee_law_feasible line 95
  12. theorem OAI.MatchingEntropyBounds.Refined.klee_uniform_mem line 99
  13. theorem OAI.MatchingEntropyBounds.Refined.klee_entropy_law line 102
  14. theorem OAI.MatchingEntropyBounds.Refined.klee_uniform_extend line 106
  15. theorem OAI.MatchingEntropyBounds.Refined.klee_law_expand line 111
  16. theorem OAI.MatchingEntropyBounds.Refined.klee_triangle_expand line 122
  17. theorem OAI.MatchingEntropyBounds.Refined.klee_zero_matching line 130
  18. theorem OAI.MatchingEntropyBounds.Refined.klee_zero_polytope line 140
  19. theorem OAI.MatchingEntropyBounds.Refined.klee_zero_minimal line 151
  20. theorem OAI.MatchingEntropyBounds.Refined.klee_minimal line 169
  21. theorem OAI.MatchingEntropyBounds.Refined.klee_dimension line 179
  22. theorem OAI.MatchingEntropyBounds.Refined.klee_zero_mean line 183
  23. theorem OAI.MatchingEntropyBounds.Refined.klee_unique_law line 199
  24. theorem OAI.MatchingEntropyBounds.Refined.klee_maxEntropy line 224
  25. theorem OAI.MatchingEntropyBounds.Refined.klee_entropy_terms line 229
  26. theorem OAI.MatchingEntropyBounds.Refined.klee_sharp_face line 247
  27. theorem OAI.MatchingEntropyBounds.Refined.coefficient_obstruction_scalar line 259
  28. theorem OAI.MatchingEntropyBounds.Refined.universal_coefficient_obstruction line 270
  29. theorem OAI.MatchingEntropyBounds.Refined.simple_coefficient_obstruction line 281