OAI/Combinatorics/MatchingEntropy/Degenerate.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatchingEntropyBounds.Refined.empty_conventions line 16
2. theorem OAI.MatchingEntropyBounds.Refined.no_matching_polytope line 48
3. theorem OAI.MatchingEntropyBounds.Refined.zero_selected_bound line 64
4. theorem OAI.MatchingEntropyBounds.Refined.zero_regular line 69
5. theorem OAI.MatchingEntropyBounds.Refined.one_selected_bound line 84
6. theorem OAI.MatchingEntropyBounds.Refined.one_partition_exact line 88
7. theorem OAI.MatchingEntropyBounds.Refined.pointwise_endpoints line 107