OAI/Combinatorics/IndependentSets/Expansion/ExpanderTableWords.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.rotationWords line 14
2. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.rotationWords_length line 16
3. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem line 20
4. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.rotationWords_get line 26
5. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem? line 32
6. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.rotationWords_getElem?_none line 38
7. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.rotationWords_entry_lt line 42
8. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.rotationWords_lookup line 47
9. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.rotationWords_row_order line 53
10. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.decode_rotationWords line 58
11. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.decoded_lookup line 62
12. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.decoded_coordinate_lookup line 68
13. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_eq line 75
14. theorem OAI.IndependentSetsGames.Foundations.PCP.ExpanderTableWords.encode_rotationWords_length_le line 79