OAI/Computability/VertexCover/PCP/AlphabetGraph.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.PCP.AlphabetGraph.Address line 17
  2. abbrev OAI.UniqueGames.Foundations.PCP.AlphabetGraph.LocalEvent line 19
  3. abbrev OAI.UniqueGames.Foundations.PCP.AlphabetGraph.Event line 22
  4. abbrev OAI.UniqueGames.Foundations.PCP.AlphabetGraph.legal line 26
  5. instance OAI.UniqueGames.Foundations.PCP.AlphabetGraph.legalDecidable line 29
  6. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.restrictTape line 33
  7. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.extendTape line 36
  8. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.globalizeQuery line 40
  9. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.verifier line 45
  10. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.vertexBlock line 52
  11. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.edgeOracle line 55
  12. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.oracleAnswer_globalize line 60
  13. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.response_eq_local line 72
  14. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.eventReject line 85
  15. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.eventReject_eq_local line 90
  16. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.expect_prod line 103
  17. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.localAverage line 108
  18. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.expect_restrict_five line 111
  19. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.localAverage_eq_tester line 149
  20. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.average line 167
  21. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.average_eq_testers line 172
  22. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.decodedLabeling line 181
  23. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.local_gap line 184
  24. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.average_gap line 201
  25. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.expect_rejection_eq_count line 209
  26. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.average_eq_count line 222
  27. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.card_event line 229
  28. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.card_localEvent line 235
  29. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.card_address line 242
  30. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.rejection_count_bound line 248
  31. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.honestAssignment line 275
  32. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.honest_vertexBlock line 280
  33. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.honest_edgeOracle line 284
  34. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.honest_event line 293
  35. def OAI.UniqueGames.Foundations.PCP.AlphabetGraph.graph line 305
  36. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.perfect_completeness line 310
  37. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.gap_transfer line 316
  38. theorem OAI.UniqueGames.Foundations.PCP.AlphabetGraph.alphabet_card line 342