OAI/Combinatorics/IndependentSets/PCP/AssignmentTester.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.truth line 16
2. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.disagree line 18
3. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.truth_nonneg line 20
4. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.disagree_nonneg line 22
5. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.disagree_eq line 25
6. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.disagree_xor_le line 29
7. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.parity line 33
8. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.bitSign_parity line 36
9. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.bitSign_injective line 44
10. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.parity_xor line 48
11. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.cubeXor_comm line 54
12. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.cubeXor_right_twice line 59
13. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.expect_cubeXor line 65
14. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.distance line 80
15. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.distance_nonneg line 83
16. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.distance_parity line 89
17. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.blrReject line 97
18. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.blrReject_nonneg line 100
19. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.blr_correlation line 107
20. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.blrReject_fourier line 126
21. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.blr_near_parity line 134
22. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.selfCorrect line 164
23. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.parity_selfCorrect line 167
24. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.selfCorrect_error line 172
25. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.singleMask line 186
26. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.flipAt line 188
27. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.flipAt_twice line 192
28. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.flipAt_eq_xor line 197
29. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.expect_flipAt line 201
30. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.walsh_singleMask line 206
31. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.parity_singleMask line 216
32. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.parity_flipAt line 220
33. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.cubeAnd line 225
34. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.andLawFailure line 227
35. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.andLawFailure_flipAt_second line 230
36. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.four_truth_lower line 247
37. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.parity_and_rejection line 251
38. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.truth_xor line 280
39. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.disagree_triangle line 283
40. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.and_disagree_transfer line 287
41. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.andReject line 293
42. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.unitReject line 298
43. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.inputReject line 303
44. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.testerReject line 306
45. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.andReject_nonneg line 309
46. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.unitReject_nonneg line 322
47. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.inputReject_nonneg line 328
48. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.andReject_transfer line 336
49. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.parity_zero line 360
50. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.unitReject_zero_parity line 365
51. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.parity_singleMask_eval line 378
52. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.inputReject_transfer line 383
53. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.tester_proximity_soundness line 400
54. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.selfCorrect_dictator line 448
55. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.tester_perfect_completeness line 454
56. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.eventQueries line 466
57. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.eventAccepts line 482
58. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.oracleAnswer line 488
59. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.eventReject line 491
60. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.truth_not_decide_eq line 496
61. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.eventReject_blr line 500
62. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.eventReject_and line 507
63. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.eventReject_unit line 516
64. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.eventReject_input line 527
65. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.event_perfect_completeness line 535
66. def OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.explicitTesterReject line 550
67. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.explicitTesterReject_eq line 554
68. theorem OAI.IndependentSetsGames.Foundations.PCP.AssignmentTester.explicit_proximity_soundness line 561