OAI/Combinatorics/IndependentSets/Expansion/ExpanderTables.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.rowIndex line 10
2. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.rowIndex_val line 12
3. structure OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.Table line 15
4. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.reverseIndex line 19
5. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.lookup line 22
6. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.lookup_involutive line 25
7. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.graph line 32
8. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.graph_rot line 36
9. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.ofGraph line 39
10. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.lookup_ofGraph line 47
11. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.graph_ext line 52
12. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.graph_ofGraph line 60
13. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.row_count line 63
14. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.vertexIndex line 66
15. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.stepGraph line 69
16. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.step line 77
17. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.stepLookup line 81
18. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.lookup_step line 95
19. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.step_certificate line 107
20. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.initial line 118
21. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.initial_certificate line 121
22. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.vertexCount line 131
23. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.vertexCount_eq line 135
24. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.vertexCount_positive line 140
25. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.family line 145
26. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.family_certificate line 150
27. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.family_row_count line 161
28. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTables.exists_base_table line 165