OAI/Computability/MinUncut/PCP/GraphTableComplexity.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial line 12
2. theorem OAI.MinUncutGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial_eval line 15
3. theorem OAI.MinUncutGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial_mono line 19
4. theorem OAI.MinUncutGames.Foundations.PCP.GraphTableComplexity.rowBound_le_polynomial line 25
5. theorem OAI.MinUncutGames.Foundations.PCP.GraphTableComplexity.generic_size_add_two_le_bits line 35
6. theorem OAI.MinUncutGames.Foundations.PCP.GraphTableComplexity.generic_bits_le_polynomial line 41
7. theorem OAI.MinUncutGames.Foundations.PCP.GraphTableComplexity.generic_bits_le_of_size_le line 47
8. theorem OAI.MinUncutGames.Foundations.PCP.GraphTableComplexity.size_add_two_le_bits line 52
9. theorem OAI.MinUncutGames.Foundations.PCP.GraphTableComplexity.bits_le_polynomial line 58
10. theorem OAI.MinUncutGames.Foundations.PCP.GraphTableComplexity.bits_le_of_size_le line 64
11. abbrev OAI.MinUncutGames.Foundations.PCP.AmplificationRound.Label line 77
12. abbrev OAI.MinUncutGames.Foundations.PCP.AmplificationRound.Addresses line 78
13. abbrev OAI.MinUncutGames.Foundations.PCP.AmplificationRound.PoweredAlphabet line 79
14. instance OAI.MinUncutGames.Foundations.PCP.AmplificationRound.(instance at line 82) line 82
15. instance OAI.MinUncutGames.Foundations.PCP.AmplificationRound.(instance at line 83) line 83
16. abbrev OAI.MinUncutGames.Foundations.PCP.AmplificationRound.PoweredDart line 88
17. instance OAI.MinUncutGames.Foundations.PCP.AmplificationRound.(instance at line 92) line 92
18. def OAI.MinUncutGames.Foundations.PCP.AmplificationRound.selectors line 94
19. def OAI.MinUncutGames.Foundations.PCP.AmplificationRound.powered line 101
20. abbrev OAI.MinUncutGames.Foundations.PCP.AmplificationRound.Vertex line 107
21. abbrev OAI.MinUncutGames.Foundations.PCP.AmplificationRound.Dart line 112
22. instance OAI.MinUncutGames.Foundations.PCP.AmplificationRound.(instance at line 115) line 115
23. instance OAI.MinUncutGames.Foundations.PCP.AmplificationRound.(instance at line 124) line 124
24. instance OAI.MinUncutGames.Foundations.PCP.AmplificationRound.(instance at line 127) line 127
25. def OAI.MinUncutGames.Foundations.PCP.AmplificationRound.graph line 129
26. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationRound.powered_completeness line 134
27. theorem OAI.MinUncutGames.Foundations.PCP.AmplificationRound.completeness line 147
28. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWitness.iterate_mul_const line 165
29. def OAI.MinUncutGames.Foundations.PCP.PoweringWitness.endpointWitness line 178
30. def OAI.MinUncutGames.Foundations.PCP.PoweringWitness.vertexWitness line 184
31. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWitness.endpoint_lower_bound line 189
32. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWitness.lazy_middle_witness_mean line 224
33. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMomentBound.symmetric_gap_matrix_sum line 266
34. def OAI.MinUncutGames.Foundations.PCP.PoweringMomentBound.windowIndex line 321
35. def OAI.MinUncutGames.Foundations.PCP.PoweringMomentBound.windowEvent line 326
36. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMomentBound.window_second_moment_eq line 330
37. theorem OAI.MinUncutGames.Foundations.PCP.PoweringMomentBound.window_second_moment_le line 354
38. theorem OAI.MinUncutGames.Foundations.PCP.PoweringNumeric.min_density_ratio line 370
39. theorem OAI.MinUncutGames.Foundations.PCP.PoweringNumeric.count_moment_ratio_lower line 396
40. def OAI.MinUncutGames.Foundations.PCP.PoweringSoundness.center line 434
41. theorem OAI.MinUncutGames.Foundations.PCP.PoweringSoundness.le_center line 436
42. def OAI.MinUncutGames.Foundations.PCP.PoweringSoundness.gain line 444
43. def OAI.MinUncutGames.Foundations.PCP.PoweringSoundness.decodedError line 451
44. def OAI.MinUncutGames.Foundations.PCP.PoweringSoundness.poweredRejection line 456
45. theorem OAI.MinUncutGames.Foundations.PCP.PoweringSoundness.witness_bit_eq line 462
46. theorem OAI.MinUncutGames.Foundations.PCP.PoweringSoundness.modal_witness_mean line 475
47. theorem OAI.MinUncutGames.Foundations.PCP.PoweringSoundness.rejection_lower_bound line 500
48. theorem OAI.MinUncutGames.Foundations.PCP.PoweringGap.gain_nonneg line 604
49. theorem OAI.MinUncutGames.Foundations.PCP.PoweringGap.uniform_count_gap line 613