OAI/Computability/DirectedFeedback/Games/CayleySpectral.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.PCP.CayleySpectral.zeroFrequency line 18
2. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.cubeXor_cancel_right line 20
3. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.cubeXor_assoc line 25
4. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.cubeXor_zeroFrequency line 31
5. def OAI.DFVSGames.Foundations.PCP.CayleySpectral.xorTranslation line 36
6. def OAI.DFVSGames.Foundations.PCP.CayleySpectral.rotate line 42
7. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.rotate_involutive line 45
8. def OAI.DFVSGames.Foundations.PCP.CayleySpectral.cayleyGraph line 50
9. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.cayleyGraph_rot line 58
10. def OAI.DFVSGames.Foundations.PCP.CayleySpectral.splitPortWord line 61
11. def OAI.DFVSGames.Foundations.PCP.CayleySpectral.powerGenerators line 69
12. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.wordEnd_eq_powerGenerators line 73
13. def OAI.DFVSGames.Foundations.PCP.CayleySpectral.cayleyAverage line 86
14. def OAI.DFVSGames.Foundations.PCP.CayleySpectral.eigenvalue line 89
15. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.averagingOperator_cayleyGraph line 93
16. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.coefficient_zeroFrequency line 96
17. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.coefficient_xorTranslation line 100
18. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.cayleyAverage_walsh line 121
19. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.coefficient_cayleyAverage line 129
20. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.eigenvalue_powerGenerators line 146
21. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.power_port_card line 171
22. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.seven_power_port_card line 175
23. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.cayley_energy_contraction line 179
24. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.cayley_spectralCertificate line 212
25. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.power_eigenvalue_bound line 223
26. theorem OAI.DFVSGames.Foundations.PCP.CayleySpectral.sevenStep_halfCertificate line 234
27. abbrev OAI.DFVSGames.Foundations.PCP.Expanders.Generators line 257
28. def OAI.DFVSGames.Foundations.PCP.Expanders.badFrequency line 259
29. def OAI.DFVSGames.Foundations.PCP.Expanders.badMass line 263
30. theorem OAI.DFVSGames.Foundations.PCP.Expanders.badFrequency_nonnegative line 266
31. theorem OAI.DFVSGames.Foundations.PCP.Expanders.mean_badFrequency_le line 271
32. theorem OAI.DFVSGames.Foundations.PCP.Expanders.mean_badMass_le line 283
33. theorem OAI.DFVSGames.Foundations.PCP.Expanders.exists_generators line 295
34. def OAI.DFVSGames.Foundations.PCP.Expanders.baseDimension line 316
35. def OAI.DFVSGames.Foundations.PCP.Expanders.initialDegree line 317
36. def OAI.DFVSGames.Foundations.PCP.Expanders.initialQuarterDegree line 318
37. def OAI.DFVSGames.Foundations.PCP.Expanders.basePower line 319
38. theorem OAI.DFVSGames.Foundations.PCP.Expanders.base_arithmetic line 321
39. theorem OAI.DFVSGames.Foundations.PCP.Expanders.exists_initial_generators line 333
40. abbrev OAI.DFVSGames.Foundations.PCP.Expanders.BaseVertex line 339
41. abbrev OAI.DFVSGames.Foundations.PCP.Expanders.BasePort line 340
42. def OAI.DFVSGames.Foundations.PCP.Expanders.baseDegree line 341
43. theorem OAI.DFVSGames.Foundations.PCP.Expanders.card_basePort line 343
44. theorem OAI.DFVSGames.Foundations.PCP.Expanders.card_baseVertex line 348
45. theorem OAI.DFVSGames.Foundations.PCP.Expanders.exists_baseGraph line 352
46. def OAI.DFVSGames.Foundations.PCP.GraphTransport.reindex line 374
47. theorem OAI.DFVSGames.Foundations.PCP.GraphTransport.reindex_rot line 386
48. theorem OAI.DFVSGames.Foundations.PCP.GraphTransport.operator_reindex line 396
49. theorem OAI.DFVSGames.Foundations.PCP.GraphTransport.energy_reindex line 405
50. theorem OAI.DFVSGames.Foundations.PCP.GraphTransport.reindex_spectralCertificate line 409
51. def OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.involutionEquiv line 438
52. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.palindrome_involutive line 444
53. def OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.squareFirst line 451
54. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.squareFirst_involutive line 455
55. def OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.squareSwap line 461
56. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.squareSwap_involutive line 463
57. def OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.square line 467
58. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.square_rot_apply line 475
59. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.square_next line 481
60. def OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.cloudFirst line 484
61. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.cloudFirst_involutive line 489
62. def OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.crossCloud line 496
63. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.crossCloud_involutive line 499
64. def OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.zigzag line 505
65. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.zigzag_rot_apply line 513
66. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.natCard_square_ports line 521
67. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.natCard_square_edges line 524
68. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_vertices line 528
69. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_ports line 531
70. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.natCard_zigzag_edges line 534
71. def OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.cloudOperator line 541
72. def OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.graphPermutation line 544
73. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.averagingOperator_square line 547
74. theorem OAI.DFVSGames.Foundations.PCP.ZigzagGraphs.averagingOperator_zigzag line 556
75. def OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.cloudMean line 584
76. def OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.liftCloud line 587
77. def OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.projection line 589
78. def OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.centered line 592
79. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.mean_liftCloud line 594
80. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.energy_liftCloud line 600
81. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.mean_cloudMean line 604
82. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.energy_prod line 607
83. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.cloudMean_centered_zero line 611
84. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.energy_centered_eq_sub line 617
85. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.projection_energy_decomposition line 640
86. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.energy_projection_le line 645
87. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.energy_centered_le line 651
88. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.mean_sq_le_energy line 656
89. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.averaging_energy_le line 661
90. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.cloudOperator_add line 670
91. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.cloudOperator_sub line 675
92. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.cloudOperator_projection line 680
93. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.cloudOperator_centered line 686
94. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.graphPermutation_energy line 692
95. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.cloud_energy_le line 696
96. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.cloud_centered_contraction line 706
97. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.cloud_residual_bound line 718
98. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.projection_graphPermutation_projection line 727
99. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.projected_outer_bound line 732
100. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.energy_add_three_le line 746
101. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.zigzag_energy_bound line 758
102. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.square_certificate line 810
103. theorem OAI.DFVSGames.Foundations.PCP.ZigzagSpectral.square_zigzag_halfCertificate line 828