OAI/Combinatorics/IndependentSets/Expansion/CloudRounding.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.dart_rejection_count_le line 9
2. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.colorSet line 56
3. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.minoritySet line 59
4. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.directedCut line 62
5. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.disagreementSet line 65
6. abbrev OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.Nonmajor line 68
7. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.exists_max_color line 71
8. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.majority line 78
9. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.majority_maximal line 82
10. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.nonchosen_color_twice_le line 87
11. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.minorityEquiv line 106
12. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.minority_card_eq_sum line 123
13. def OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.minorityCutEmbedding line 128
14. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.minority_cut_sum_le line 154
15. theorem OAI.IndependentSetsGames.Foundations.PCP.CloudRounding.minority_expansion_bound line 161