OAI/Computability/VertexCover/PCP/ClauseVerifier.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniqueGames.Foundations.PCP.ClauseAnswer line 12
  2. inductive OAI.UniqueGames.Foundations.PCP.Slot line 18
  3. def OAI.UniqueGames.Foundations.PCP.answerAt line 24
  4. def OAI.UniqueGames.Foundations.PCP.nameAt line 29
  5. def OAI.UniqueGames.Foundations.PCP.literalValue line 34
  6. def OAI.UniqueGames.Foundations.PCP.localSatisfies line 37
  7. def OAI.UniqueGames.Foundations.PCP.honestAnswer line 42
  8. theorem OAI.UniqueGames.Foundations.PCP.honest_satisfies line 46
  9. theorem OAI.UniqueGames.Foundations.PCP.honest_answerAt line 49
  10. def OAI.UniqueGames.Foundations.PCP.matchingSlots line 54
  11. theorem OAI.UniqueGames.Foundations.PCP.matchingSlots_le line 59
  12. theorem OAI.UniqueGames.Foundations.PCP.matchingSlots_eq_three line 64
  13. def OAI.UniqueGames.Foundations.PCP.acceptedSlots line 69
  14. def OAI.UniqueGames.Foundations.PCP.clauseFailure line 72
  15. theorem OAI.UniqueGames.Foundations.PCP.local_rejection_bound line 75
  16. def OAI.UniqueGames.Foundations.PCP.clauseAt line 97
  17. abbrev OAI.UniqueGames.Foundations.PCP.RandomEvent line 100
  18. abbrev OAI.UniqueGames.Foundations.PCP.AliceStrategy line 101
  19. abbrev OAI.UniqueGames.Foundations.PCP.BobStrategy line 102
  20. def OAI.UniqueGames.Foundations.PCP.accepts line 104
  21. def OAI.UniqueGames.Foundations.PCP.acceptedCount line 109
  22. def OAI.UniqueGames.Foundations.PCP.failureCount line 115
  23. theorem OAI.UniqueGames.Foundations.PCP.total_rejection_bound line 120
  24. def OAI.UniqueGames.Foundations.PCP.allIndices line 131
  25. theorem OAI.UniqueGames.Foundations.PCP.hastad_basic_verifier_soundness line 134
  26. theorem OAI.UniqueGames.Foundations.PCP.honest_accepts line 145
  27. theorem OAI.UniqueGames.Foundations.PCP.verifier_completeness line 153
  28. abbrev OAI.UniqueGames.Foundations.PCP.LeftLabel line 160
  29. def OAI.UniqueGames.Foundations.PCP.edgeProjection line 163
  30. theorem OAI.UniqueGames.Foundations.PCP.verifier_eq_projection line 166
  31. def OAI.UniqueGames.Foundations.PCP.eventsAt line 173
  32. def OAI.UniqueGames.Foundations.PCP.enumerateEvents line 176
  33. theorem OAI.UniqueGames.Foundations.PCP.length_enumerateEvents line 181
  34. theorem OAI.UniqueGames.Foundations.PCP.accepted_eventsAt line 190
  35. theorem OAI.UniqueGames.Foundations.PCP.accepted_enumerateEvents line 202
  36. def OAI.UniqueGames.Foundations.PCP.allEvents line 212
  37. theorem OAI.UniqueGames.Foundations.PCP.length_allEvents line 215
  38. theorem OAI.UniqueGames.Foundations.PCP.allEvents_nonempty line 219
  39. theorem OAI.UniqueGames.Foundations.PCP.verifier_event_soundness line 228
  40. def OAI.UniqueGames.Foundations.PCP.occurrencesAt line 238
  41. def OAI.UniqueGames.Foundations.PCP.occurrenceCount line 243
  42. theorem OAI.UniqueGames.Foundations.PCP.variable_eventsAt line 248
  43. theorem OAI.UniqueGames.Foundations.PCP.variable_enumerateEvents line 258
  44. theorem OAI.UniqueGames.Foundations.PCP.regular_bob_marginal line 269