OAI/Combinatorics/IndependentSets/Expansion/ZigzagSpectral.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.cloudMean line 14
2. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.liftCloud line 17
3. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.projection line 19
4. def OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.centered line 22
5. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.mean_liftCloud line 24
6. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.energy_liftCloud line 30
7. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.mean_cloudMean line 34
8. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.energy_prod line 37
9. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.cloudMean_centered_zero line 41
10. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.energy_centered_eq_sub line 47
11. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.projection_energy_decomposition line 70
12. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.energy_projection_le line 75
13. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.energy_centered_le line 81
14. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.mean_sq_le_energy line 86
15. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.averaging_energy_le line 91
16. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.cloudOperator_add line 100
17. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.cloudOperator_sub line 105
18. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.cloudOperator_projection line 110
19. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.cloudOperator_centered line 116
20. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.graphPermutation_energy line 122
21. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.cloud_energy_le line 126
22. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.cloud_centered_contraction line 136
23. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.cloud_residual_bound line 148
24. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.projection_graphPermutation_projection line 157
25. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.projected_outer_bound line 162
26. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.energy_add_three_le line 176
27. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.zigzag_energy_bound line 188
28. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.square_certificate line 240
29. theorem OAI.IndependentSetsGames.Foundations.PCP.ZigzagSpectral.square_zigzag_halfCertificate line 258