OAI/Combinatorics/IndependentSets/Expansion/CayleySpectral.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.zeroFrequency line 18
2. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.cubeXor_cancel_right line 20
3. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.cubeXor_assoc line 25
4. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.cubeXor_zeroFrequency line 31
5. def OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.xorTranslation line 36
6. def OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.rotate line 42
7. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.rotate_involutive line 45
8. def OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.cayleyGraph line 50
9. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.cayleyGraph_rot line 58
10. def OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.splitPortWord line 61
11. def OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.powerGenerators line 69
12. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.wordEnd_eq_powerGenerators line 73
13. def OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.cayleyAverage line 85
14. def OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.eigenvalue line 88
15. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.averagingOperator_cayleyGraph line 92
16. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.coefficient_zeroFrequency line 95
17. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.coefficient_xorTranslation line 99
18. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.cayleyAverage_walsh line 120
19. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.coefficient_cayleyAverage line 128
20. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.eigenvalue_powerGenerators line 145
21. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.power_port_card line 170
22. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.seven_power_port_card line 174
23. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.cayley_energy_contraction line 178
24. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.cayley_spectralCertificate line 211
25. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.power_eigenvalue_bound line 222
26. theorem OAI.IndependentSetsGames.Foundations.PCP.CayleySpectral.sevenStep_halfCertificate line 233