OAI/Combinatorics/MatchingEntropy/Basic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatchingEntropyBounds.LooplessGraph.indicator_nonneg line 17
2. theorem OAI.MatchingEntropyBounds.LooplessGraph.indicator_le_one line 23
3. theorem OAI.MatchingEntropyBounds.LooplessGraph.continuous_mean line 29
4. def OAI.MatchingEntropyBounds.LooplessGraph.meanLinear line 33
5. theorem OAI.MatchingEntropyBounds.LooplessGraph.mean_mem_polytope line 43
6. theorem OAI.MatchingEntropyBounds.LooplessGraph.mean_single line 54
7. theorem OAI.MatchingEntropyBounds.LooplessGraph.mem_polytope_iff line 62
8. theorem OAI.MatchingEntropyBounds.LooplessGraph.compact_feasibleLaws line 78
9. theorem OAI.MatchingEntropyBounds.LooplessGraph.compact_polytope line 84