OAI/Computability/DirectedFeedback/Encoding/FinalCNFPattern.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.Label line 12
2. abbrev OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.labelEquiv line 14
3. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.labelEquiv_val line 16
4. def OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.labelIndex line 21
5. def OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.labelBits line 23
6. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.labelBits_labelIndex line 25
7. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.labelIndex_labelBits line 28
8. def OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.leftHalf line 31
9. def OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.rightHalf line 34
10. def OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.relationAddress line 37
11. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.relationAddress_val line 40
12. def OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex line 45
13. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex_eq line 48
14. def OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.tableGraph line 51
15. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.tableGraph_tail line 55
16. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.tableGraph_reverse line 58
17. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.tableGraph_accepts line 61
18. abbrev OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.tableVerifier line 66
19. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.relation_lookup_eq_verifier_accepts line 69
20. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.pattern_lookup_eq_verifier_accepts line 74
21. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.verifier_accepts_eq_lookup line 79
22. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.buffer_lookup_eq_verifier_accepts line 84
23. theorem OAI.DFVSGames.Foundations.Complexity.FinalCNFPattern.pattern_buffer_lookup_eq_verifier_accepts line 91
24. def OAI.DFVSGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial line 106
25. theorem OAI.DFVSGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial_eval line 109
26. theorem OAI.DFVSGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial_mono line 113
27. theorem OAI.DFVSGames.Foundations.PCP.GraphTableComplexity.rowBound_le_polynomial line 119
28. theorem OAI.DFVSGames.Foundations.PCP.GraphTableComplexity.generic_size_add_two_le_bits line 129
29. theorem OAI.DFVSGames.Foundations.PCP.GraphTableComplexity.generic_bits_le_polynomial line 135
30. theorem OAI.DFVSGames.Foundations.PCP.GraphTableComplexity.generic_bits_le_of_size_le line 141
31. theorem OAI.DFVSGames.Foundations.PCP.GraphTableComplexity.size_add_two_le_bits line 146
32. theorem OAI.DFVSGames.Foundations.PCP.GraphTableComplexity.bits_le_polynomial line 152
33. theorem OAI.DFVSGames.Foundations.PCP.GraphTableComplexity.bits_le_of_size_le line 158
34. abbrev OAI.DFVSGames.Foundations.PCP.AmplificationRound.Label line 169
35. abbrev OAI.DFVSGames.Foundations.PCP.AmplificationRound.Addresses line 170
36. abbrev OAI.DFVSGames.Foundations.PCP.AmplificationRound.PoweredAlphabet line 171
37. instance OAI.DFVSGames.Foundations.PCP.AmplificationRound.(instance at line 174) line 174
38. instance OAI.DFVSGames.Foundations.PCP.AmplificationRound.(instance at line 175) line 175
39. abbrev OAI.DFVSGames.Foundations.PCP.AmplificationRound.PoweredDart line 180
40. instance OAI.DFVSGames.Foundations.PCP.AmplificationRound.(instance at line 184) line 184
41. def OAI.DFVSGames.Foundations.PCP.AmplificationRound.selectors line 186
42. def OAI.DFVSGames.Foundations.PCP.AmplificationRound.powered line 193
43. abbrev OAI.DFVSGames.Foundations.PCP.AmplificationRound.Vertex line 199
44. abbrev OAI.DFVSGames.Foundations.PCP.AmplificationRound.Dart line 204
45. instance OAI.DFVSGames.Foundations.PCP.AmplificationRound.(instance at line 207) line 207
46. instance OAI.DFVSGames.Foundations.PCP.AmplificationRound.(instance at line 216) line 216
47. instance OAI.DFVSGames.Foundations.PCP.AmplificationRound.(instance at line 219) line 219
48. def OAI.DFVSGames.Foundations.PCP.AmplificationRound.graph line 221
49. theorem OAI.DFVSGames.Foundations.PCP.AmplificationRound.powered_completeness line 226
50. theorem OAI.DFVSGames.Foundations.PCP.AmplificationRound.completeness line 239
51. theorem OAI.DFVSGames.Foundations.PCP.PoweringWitness.iterate_mul_const line 255
52. def OAI.DFVSGames.Foundations.PCP.PoweringWitness.endpointWitness line 268
53. def OAI.DFVSGames.Foundations.PCP.PoweringWitness.vertexWitness line 274
54. theorem OAI.DFVSGames.Foundations.PCP.PoweringWitness.endpoint_lower_bound line 279
55. theorem OAI.DFVSGames.Foundations.PCP.PoweringWitness.lazy_middle_witness_mean line 314
56. theorem OAI.DFVSGames.Foundations.PCP.PoweringMomentBound.symmetric_gap_matrix_sum line 354
57. def OAI.DFVSGames.Foundations.PCP.PoweringMomentBound.windowIndex line 409
58. def OAI.DFVSGames.Foundations.PCP.PoweringMomentBound.windowEvent line 414
59. theorem OAI.DFVSGames.Foundations.PCP.PoweringMomentBound.window_second_moment_eq line 418
60. theorem OAI.DFVSGames.Foundations.PCP.PoweringMomentBound.window_second_moment_le line 442
61. theorem OAI.DFVSGames.Foundations.PCP.PoweringNumeric.min_density_ratio line 456
62. theorem OAI.DFVSGames.Foundations.PCP.PoweringNumeric.count_moment_ratio_lower line 482
63. def OAI.DFVSGames.Foundations.PCP.PoweringSoundness.center line 518
64. theorem OAI.DFVSGames.Foundations.PCP.PoweringSoundness.le_center line 520
65. def OAI.DFVSGames.Foundations.PCP.PoweringSoundness.gain line 528
66. def OAI.DFVSGames.Foundations.PCP.PoweringSoundness.decodedError line 535
67. def OAI.DFVSGames.Foundations.PCP.PoweringSoundness.poweredRejection line 540
68. theorem OAI.DFVSGames.Foundations.PCP.PoweringSoundness.witness_bit_eq line 547
69. theorem OAI.DFVSGames.Foundations.PCP.PoweringSoundness.modal_witness_mean line 560
70. theorem OAI.DFVSGames.Foundations.PCP.PoweringSoundness.rejection_lower_bound line 585
71. theorem OAI.DFVSGames.Foundations.PCP.PoweringGap.gain_nonneg line 687
72. theorem OAI.DFVSGames.Foundations.PCP.PoweringGap.uniform_count_gap line 696