OAI/Computability/VertexCover/PCP/CayleySpectral.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.CayleySpectral.zeroFrequency line 20
  2. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.cubeXor_cancel_right line 22
  3. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.cubeXor_assoc line 27
  4. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.cubeXor_zeroFrequency line 33
  5. def OAI.UniqueGames.Foundations.PCP.CayleySpectral.xorTranslation line 38
  6. def OAI.UniqueGames.Foundations.PCP.CayleySpectral.rotate line 44
  7. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.rotate_involutive line 47
  8. def OAI.UniqueGames.Foundations.PCP.CayleySpectral.cayleyGraph line 52
  9. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.cayleyGraph_rot line 60
  10. def OAI.UniqueGames.Foundations.PCP.CayleySpectral.splitPortWord line 63
  11. def OAI.UniqueGames.Foundations.PCP.CayleySpectral.powerGenerators line 71
  12. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.wordEnd_eq_powerGenerators line 75
  13. def OAI.UniqueGames.Foundations.PCP.CayleySpectral.cayleyAverage line 87
  14. def OAI.UniqueGames.Foundations.PCP.CayleySpectral.eigenvalue line 90
  15. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.averagingOperator_cayleyGraph line 94
  16. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.coefficient_zeroFrequency line 97
  17. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.coefficient_xorTranslation line 101
  18. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.cayleyAverage_walsh line 122
  19. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.coefficient_cayleyAverage line 130
  20. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.eigenvalue_powerGenerators line 147
  21. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.power_port_card line 172
  22. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.seven_power_port_card line 176
  23. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.cayley_energy_contraction line 180
  24. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.cayley_spectralCertificate line 213
  25. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.power_eigenvalue_bound line 224
  26. theorem OAI.UniqueGames.Foundations.PCP.CayleySpectral.sevenStep_halfCertificate line 235