OAI/Computability/UniqueGames/PCP/SourceIncidence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Outer.SourceIncidence.incidence line 20
  2. theorem OAI.UniqueGamesTheorem.Outer.SourceIncidence.names_distinct line 24
  3. theorem OAI.UniqueGamesTheorem.Outer.SourceIncidence.uniform_probability_eq_expect line 31
  4. theorem OAI.UniqueGamesTheorem.Outer.SourceIncidence.paritySuccess_eq line 43
  5. theorem OAI.UniqueGamesTheorem.Outer.SourceIncidence.paritySuccess_input line 63
  6. def OAI.UniqueGamesTheorem.Outer.SourceIncidence.input line 73
  7. def OAI.UniqueGamesTheorem.Outer.SourceIncidence.source line 77
  8. theorem OAI.UniqueGamesTheorem.Outer.SourceIncidence.source_distinct line 80
  9. theorem OAI.UniqueGamesTheorem.Outer.SourceIncidence.source_complete line 84
  10. theorem OAI.UniqueGamesTheorem.Outer.SourceIncidence.source_sound line 101
  11. def OAI.UniqueGamesTheorem.Outer.SourceIncidence.ordinaryGame line 117
  12. theorem OAI.UniqueGamesTheorem.Outer.SourceIncidence.ordinaryGame_projection line 121
  13. theorem OAI.UniqueGamesTheorem.Outer.SourceIncidence.ordinaryGame_sound line 125