OAI/Combinatorics/IndependentSets/PCP/AlphabetGraph.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.Address line 14
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.LocalEvent line 16
  3. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.Event line 19
  4. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.legal line 23
  5. instance OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.legalDecidable line 26
  6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.restrictTape line 30
  7. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.extendTape line 33
  8. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.globalizeQuery line 37
  9. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.verifier line 42
  10. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.vertexBlock line 49
  11. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.edgeOracle line 52
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.oracleAnswer_globalize line 57
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.response_eq_local line 69
  14. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.eventReject line 82
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.eventReject_eq_local line 87
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.expect_prod line 100
  17. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.localAverage line 105
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.expect_restrict_five line 108
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.localAverage_eq_tester line 145
  20. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.average line 163
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.average_eq_testers line 168
  22. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.decodedLabeling line 177
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.local_gap line 180
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.average_gap line 197
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.expect_rejection_eq_count line 205
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.average_eq_count line 218
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.card_event line 225
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.card_localEvent line 230
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.card_address line 237
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.rejection_count_bound line 243
  31. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.honestAssignment line 270
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.honest_vertexBlock line 275
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.honest_edgeOracle line 279
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.honest_event line 288
  35. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.graph line 300
  36. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.perfect_completeness line 305
  37. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.gap_transfer line 311
  38. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetGraph.alphabet_card line 337