OAI/Combinatorics/IndependentSets/PCP/ClauseVerifier.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.IndependentSetsGames.Foundations.PCP.ClauseAnswer line 10
  2. inductive OAI.IndependentSetsGames.Foundations.PCP.Slot line 16
  3. def OAI.IndependentSetsGames.Foundations.PCP.answerAt line 22
  4. def OAI.IndependentSetsGames.Foundations.PCP.nameAt line 27
  5. def OAI.IndependentSetsGames.Foundations.PCP.literalValue line 32
  6. def OAI.IndependentSetsGames.Foundations.PCP.localSatisfies line 35
  7. def OAI.IndependentSetsGames.Foundations.PCP.honestAnswer line 40
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.honest_satisfies line 44
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.honest_answerAt line 47
  10. def OAI.IndependentSetsGames.Foundations.PCP.matchingSlots line 52
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.matchingSlots_le line 57
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.matchingSlots_eq_three line 62
  13. def OAI.IndependentSetsGames.Foundations.PCP.acceptedSlots line 67
  14. def OAI.IndependentSetsGames.Foundations.PCP.clauseFailure line 70
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.local_rejection_bound line 73
  16. def OAI.IndependentSetsGames.Foundations.PCP.clauseAt line 95
  17. abbrev OAI.IndependentSetsGames.Foundations.PCP.RandomEvent line 98
  18. abbrev OAI.IndependentSetsGames.Foundations.PCP.AliceStrategy line 99
  19. abbrev OAI.IndependentSetsGames.Foundations.PCP.BobStrategy line 100
  20. def OAI.IndependentSetsGames.Foundations.PCP.accepts line 102
  21. def OAI.IndependentSetsGames.Foundations.PCP.acceptedCount line 107
  22. def OAI.IndependentSetsGames.Foundations.PCP.failureCount line 113
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.total_rejection_bound line 118
  24. def OAI.IndependentSetsGames.Foundations.PCP.allIndices line 129
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.hastad_basic_verifier_soundness line 132
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.honest_accepts line 143
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.verifier_completeness line 151
  28. abbrev OAI.IndependentSetsGames.Foundations.PCP.LeftLabel line 158
  29. def OAI.IndependentSetsGames.Foundations.PCP.edgeProjection line 161
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.verifier_eq_projection line 164
  31. def OAI.IndependentSetsGames.Foundations.PCP.eventsAt line 172
  32. def OAI.IndependentSetsGames.Foundations.PCP.enumerateEvents line 175
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.length_enumerateEvents line 180
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.accepted_eventsAt line 189
  35. theorem OAI.IndependentSetsGames.Foundations.PCP.accepted_enumerateEvents line 201
  36. def OAI.IndependentSetsGames.Foundations.PCP.allEvents line 211
  37. theorem OAI.IndependentSetsGames.Foundations.PCP.length_allEvents line 214
  38. theorem OAI.IndependentSetsGames.Foundations.PCP.allEvents_nonempty line 218
  39. theorem OAI.IndependentSetsGames.Foundations.PCP.verifier_event_soundness line 227
  40. def OAI.IndependentSetsGames.Foundations.PCP.occurrencesAt line 237
  41. def OAI.IndependentSetsGames.Foundations.PCP.occurrenceCount line 242
  42. theorem OAI.IndependentSetsGames.Foundations.PCP.variable_eventsAt line 247
  43. theorem OAI.IndependentSetsGames.Foundations.PCP.variable_enumerateEvents line 257
  44. theorem OAI.IndependentSetsGames.Foundations.PCP.regular_bob_marginal line 268