OAI/Computability/VertexCover/PCP/AssignmentTester.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.truth line 18
  2. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.disagree line 20
  3. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.truth_nonneg line 22
  4. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.disagree_nonneg line 24
  5. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.disagree_eq line 27
  6. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.disagree_xor_le line 31
  7. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.parity line 35
  8. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.bitSign_parity line 38
  9. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.bitSign_injective line 46
  10. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.parity_xor line 50
  11. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.cubeXor_comm line 56
  12. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.cubeXor_right_twice line 61
  13. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.expect_cubeXor line 67
  14. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.distance line 82
  15. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.distance_nonneg line 85
  16. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.distance_parity line 91
  17. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.blrReject line 99
  18. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.blrReject_nonneg line 102
  19. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.blr_correlation line 109
  20. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.blrReject_fourier line 128
  21. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.blr_near_parity line 136
  22. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.selfCorrect line 166
  23. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.parity_selfCorrect line 169
  24. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.selfCorrect_error line 174
  25. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.singleMask line 188
  26. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.flipAt line 190
  27. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.flipAt_twice line 194
  28. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.flipAt_eq_xor line 199
  29. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.expect_flipAt line 203
  30. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.walsh_singleMask line 208
  31. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.parity_singleMask line 218
  32. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.parity_flipAt line 222
  33. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.cubeAnd line 227
  34. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.andLawFailure line 229
  35. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.andLawFailure_flipAt_second line 232
  36. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.four_truth_lower line 249
  37. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.parity_and_rejection line 253
  38. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.truth_xor line 282
  39. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.disagree_triangle line 285
  40. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.and_disagree_transfer line 289
  41. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.andReject line 295
  42. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.unitReject line 300
  43. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.inputReject line 305
  44. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.testerReject line 308
  45. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.andReject_nonneg line 311
  46. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.unitReject_nonneg line 324
  47. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.inputReject_nonneg line 330
  48. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.andReject_transfer line 338
  49. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.parity_zero line 362
  50. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.unitReject_zero_parity line 367
  51. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.parity_singleMask_eval line 380
  52. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.inputReject_transfer line 385
  53. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.tester_proximity_soundness line 402
  54. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.selfCorrect_dictator line 450
  55. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.tester_perfect_completeness line 457
  56. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.eventQueries line 469
  57. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.eventAccepts line 485
  58. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.oracleAnswer line 491
  59. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.eventReject line 494
  60. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.truth_not_decide_eq line 499
  61. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.eventReject_blr line 503
  62. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.eventReject_and line 510
  63. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.eventReject_unit line 519
  64. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.eventReject_input line 530
  65. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.event_perfect_completeness line 539
  66. def OAI.UniqueGames.Foundations.PCP.AssignmentTester.explicitTesterReject line 554
  67. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.explicitTesterReject_eq line 558
  68. theorem OAI.UniqueGames.Foundations.PCP.AssignmentTester.explicit_proximity_soundness line 565