OAI/Combinatorics/MatchingEntropy/ExpansionSequences.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MatchingEntropyBounds.Refined.KleeConstruction line 14
  2. def OAI.MatchingEntropyBounds.Refined.coloredLaw line 20
  3. theorem OAI.MatchingEntropyBounds.Refined.colored_law_eq_fiber line 28
  4. theorem OAI.MatchingEntropyBounds.Refined.colored_law_feasible line 40
  5. theorem OAI.MatchingEntropyBounds.Refined.colored_uniform_mem line 46
  6. theorem OAI.MatchingEntropyBounds.Refined.colored_entropy_law line 51
  7. theorem OAI.MatchingEntropyBounds.Refined.colored_law_expand line 58
  8. theorem OAI.MatchingEntropyBounds.Refined.colored_unique_expansion line 70
  9. theorem OAI.MatchingEntropyBounds.Refined.colored_triangle_expansion line 87
  10. theorem OAI.MatchingEntropyBounds.Refined.colored_minimal_expansion line 96
  11. theorem OAI.MatchingEntropyBounds.Refined.klee_generated_cubic line 108
  12. theorem OAI.MatchingEntropyBounds.Refined.klee_generated_minimal line 114
  13. theorem OAI.MatchingEntropyBounds.Refined.klee_generated_unique line 122
  14. theorem OAI.MatchingEntropyBounds.Refined.klee_initial_expansion_simple line 130
  15. theorem OAI.MatchingEntropyBounds.Refined.klee_generated_simple line 145
  16. theorem OAI.MatchingEntropyBounds.Refined.klee_all_expansions line 156