OAI/Computability/MinUncut/PCP/CayleySpectral.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.CayleySpectral.zeroFrequency line 17
2. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.cubeXor_cancel_right line 19
3. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.cubeXor_assoc line 24
4. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.cubeXor_zeroFrequency line 30
5. def OAI.MinUncutGames.Foundations.PCP.CayleySpectral.xorTranslation line 35
6. def OAI.MinUncutGames.Foundations.PCP.CayleySpectral.rotate line 41
7. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.rotate_involutive line 44
8. def OAI.MinUncutGames.Foundations.PCP.CayleySpectral.cayleyGraph line 49
9. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.cayleyGraph_rot line 57
10. def OAI.MinUncutGames.Foundations.PCP.CayleySpectral.splitPortWord line 60
11. def OAI.MinUncutGames.Foundations.PCP.CayleySpectral.powerGenerators line 68
12. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.wordEnd_eq_powerGenerators line 72
13. def OAI.MinUncutGames.Foundations.PCP.CayleySpectral.cayleyAverage line 85
14. def OAI.MinUncutGames.Foundations.PCP.CayleySpectral.eigenvalue line 88
15. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.averagingOperator_cayleyGraph line 92
16. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.coefficient_zeroFrequency line 95
17. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.coefficient_xorTranslation line 99
18. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.cayleyAverage_walsh line 120
19. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.coefficient_cayleyAverage line 128
20. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.eigenvalue_powerGenerators line 145
21. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.power_port_card line 170
22. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.seven_power_port_card line 174
23. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.cayley_energy_contraction line 178
24. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.cayley_spectralCertificate line 211
25. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.power_eigenvalue_bound line 222
26. theorem OAI.MinUncutGames.Foundations.PCP.CayleySpectral.sevenStep_halfCertificate line 233
27. abbrev OAI.MinUncutGames.Foundations.PCP.Expanders.Generators line 253
28. def OAI.MinUncutGames.Foundations.PCP.Expanders.badFrequency line 255
29. def OAI.MinUncutGames.Foundations.PCP.Expanders.badMass line 259
30. theorem OAI.MinUncutGames.Foundations.PCP.Expanders.badFrequency_nonnegative line 262
31. theorem OAI.MinUncutGames.Foundations.PCP.Expanders.mean_badFrequency_le line 267
32. theorem OAI.MinUncutGames.Foundations.PCP.Expanders.mean_badMass_le line 279
33. theorem OAI.MinUncutGames.Foundations.PCP.Expanders.exists_generators line 291
34. def OAI.MinUncutGames.Foundations.PCP.Expanders.baseDimension line 312
35. def OAI.MinUncutGames.Foundations.PCP.Expanders.initialDegree line 313
36. def OAI.MinUncutGames.Foundations.PCP.Expanders.initialQuarterDegree line 314
37. def OAI.MinUncutGames.Foundations.PCP.Expanders.basePower line 315
38. theorem OAI.MinUncutGames.Foundations.PCP.Expanders.base_arithmetic line 317
39. theorem OAI.MinUncutGames.Foundations.PCP.Expanders.exists_initial_generators line 329
40. abbrev OAI.MinUncutGames.Foundations.PCP.Expanders.BaseVertex line 335
41. abbrev OAI.MinUncutGames.Foundations.PCP.Expanders.BasePort line 336
42. def OAI.MinUncutGames.Foundations.PCP.Expanders.baseDegree line 337
43. theorem OAI.MinUncutGames.Foundations.PCP.Expanders.card_basePort line 339
44. theorem OAI.MinUncutGames.Foundations.PCP.Expanders.card_baseVertex line 344
45. theorem OAI.MinUncutGames.Foundations.PCP.Expanders.exists_baseGraph line 348
46. def OAI.MinUncutGames.Foundations.PCP.GraphTransport.reindex line 369
47. theorem OAI.MinUncutGames.Foundations.PCP.GraphTransport.reindex_rot line 381
48. theorem OAI.MinUncutGames.Foundations.PCP.GraphTransport.operator_reindex line 391
49. theorem OAI.MinUncutGames.Foundations.PCP.GraphTransport.energy_reindex line 400
50. theorem OAI.MinUncutGames.Foundations.PCP.GraphTransport.reindex_spectralCertificate line 404
51. def OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.involutionEquiv line 432
52. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.palindrome_involutive line 438
53. def OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.squareFirst line 445
54. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.squareFirst_involutive line 449
55. def OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.squareSwap line 455
56. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.squareSwap_involutive line 457
57. def OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.square line 461
58. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.square_rot_apply line 469
59. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.square_next line 475
60. def OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.cloudFirst line 478
61. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.cloudFirst_involutive line 483
62. def OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.crossCloud line 490
63. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.crossCloud_involutive line 493
64. def OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.zigzag line 499
65. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.zigzag_rot_apply line 507
66. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.natCard_square_ports line 515
67. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.natCard_square_edges line 518
68. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_vertices line 522
69. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_ports line 525
70. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_edges line 528
71. def OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.cloudOperator line 535
72. def OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.graphPermutation line 538
73. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.averagingOperator_square line 541
74. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagGraphs.averagingOperator_zigzag line 550
75. def OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.cloudMean line 577
76. def OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.liftCloud line 580
77. def OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.projection line 582
78. def OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.centered line 585
79. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.mean_liftCloud line 587
80. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.energy_liftCloud line 593
81. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.mean_cloudMean line 597
82. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.energy_prod line 600
83. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.cloudMean_centered_zero line 604
84. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.energy_centered_eq_sub line 610
85. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.projection_energy_decomposition line 633
86. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.energy_projection_le line 638
87. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.energy_centered_le line 644
88. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.mean_sq_le_energy line 649
89. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.averaging_energy_le line 654
90. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.cloudOperator_add line 663
91. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.cloudOperator_sub line 668
92. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.cloudOperator_projection line 673
93. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.cloudOperator_centered line 679
94. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.graphPermutation_energy line 685
95. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.cloud_energy_le line 689
96. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.cloud_centered_contraction line 699
97. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.cloud_residual_bound line 711
98. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.projection_graphPermutation_projection line 720
99. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.projected_outer_bound line 725
100. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.energy_add_three_le line 739
101. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.zigzag_energy_bound line 751
102. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.square_certificate line 803
103. theorem OAI.MinUncutGames.Foundations.PCP.ZigzagSpectral.square_zigzag_halfCertificate line 821