OAI/Computability/VertexCover/PCP/ZigzagSpectral.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.cloudMean line 16
2. def OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.liftCloud line 19
3. def OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.projection line 21
4. def OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.centered line 24
5. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.mean_liftCloud line 26
6. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.energy_liftCloud line 32
7. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.mean_cloudMean line 36
8. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.energy_prod line 39
9. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.cloudMean_centered_zero line 43
10. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.energy_centered_eq_sub line 49
11. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.projection_energy_decomposition line 72
12. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.energy_projection_le line 77
13. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.energy_centered_le line 83
14. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.mean_sq_le_energy line 88
15. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.averaging_energy_le line 93
16. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.cloudOperator_add line 102
17. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.cloudOperator_sub line 107
18. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.cloudOperator_projection line 112
19. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.cloudOperator_centered line 118
20. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.graphPermutation_energy line 124
21. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.cloud_energy_le line 128
22. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.cloud_centered_contraction line 138
23. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.cloud_residual_bound line 150
24. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.projection_graphPermutation_projection line 159
25. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.projected_outer_bound line 164
26. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.energy_add_three_le line 178
27. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.zigzag_energy_bound line 190
28. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.square_certificate line 242
29. theorem OAI.UniqueGames.Foundations.PCP.ZigzagSpectral.square_zigzag_halfCertificate line 260