OAI/Combinatorics/IndependentSets/Expansion/Expanders.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.PCP.Expanders.Generators line 16
2. def OAI.IndependentSetsGames.Foundations.PCP.Expanders.badFrequency line 18
3. def OAI.IndependentSetsGames.Foundations.PCP.Expanders.badMass line 22
4. theorem OAI.IndependentSetsGames.Foundations.PCP.Expanders.badFrequency_nonnegative line 25
5. theorem OAI.IndependentSetsGames.Foundations.PCP.Expanders.mean_badFrequency_le line 30
6. theorem OAI.IndependentSetsGames.Foundations.PCP.Expanders.mean_badMass_le line 42
7. theorem OAI.IndependentSetsGames.Foundations.PCP.Expanders.exists_generators line 54
8. def OAI.IndependentSetsGames.Foundations.PCP.Expanders.baseDimension line 75
9. def OAI.IndependentSetsGames.Foundations.PCP.Expanders.initialDegree line 76
10. def OAI.IndependentSetsGames.Foundations.PCP.Expanders.initialQuarterDegree line 77
11. def OAI.IndependentSetsGames.Foundations.PCP.Expanders.basePower line 78
12. theorem OAI.IndependentSetsGames.Foundations.PCP.Expanders.base_arithmetic line 80
13. theorem OAI.IndependentSetsGames.Foundations.PCP.Expanders.exists_initial_generators line 91
14. abbrev OAI.IndependentSetsGames.Foundations.PCP.Expanders.BaseVertex line 97
15. abbrev OAI.IndependentSetsGames.Foundations.PCP.Expanders.BasePort line 98
16. def OAI.IndependentSetsGames.Foundations.PCP.Expanders.baseDegree line 99
17. theorem OAI.IndependentSetsGames.Foundations.PCP.Expanders.card_basePort line 101
18. theorem OAI.IndependentSetsGames.Foundations.PCP.Expanders.card_baseVertex line 106
19. theorem OAI.IndependentSetsGames.Foundations.PCP.Expanders.exists_baseGraph line 110
20. def OAI.IndependentSetsGames.Foundations.PCP.GraphTransport.reindex line 130
21. theorem OAI.IndependentSetsGames.Foundations.PCP.GraphTransport.reindex_rot line 142