OAI/Computability/VertexCover/Repetition/SharedSampling.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.Repetition.TraceSeed line 50
  2. instance OAI.UniqueGames.Foundations.Repetition.traceSeedFintype line 54
  3. instance OAI.UniqueGames.Foundations.Repetition.traceSeedUniqueZero line 59
  4. def OAI.UniqueGames.Foundations.Repetition.traceList line 62
  5. def OAI.UniqueGames.Foundations.Repetition.traceSeedLaw line 66
  6. theorem OAI.UniqueGames.Foundations.Repetition.traceSeedLaw_expectation line 72
  7. def OAI.UniqueGames.Foundations.Repetition.sharedOutputLaw line 89
  8. theorem OAI.UniqueGames.Foundations.Repetition.sharedOutputLaw_weight line 97
  9. def OAI.UniqueGames.Foundations.Repetition.samplerLocal line 117
  10. def OAI.UniqueGames.Foundations.Repetition.samplerOutputLaw line 123
  11. theorem OAI.UniqueGames.Foundations.Repetition.probability_weight_le_one line 130
  12. theorem OAI.UniqueGames.Foundations.Repetition.samplerOutputLaw_diagonal line 136
  13. theorem OAI.UniqueGames.Foundations.Repetition.samplerOutputLaw_uniform_diagonal line 167
  14. theorem OAI.UniqueGames.Foundations.Repetition.samplerOutputLaw_totalVariation line 187
  15. theorem OAI.UniqueGames.Foundations.Repetition.samplerOutputLaw_arbitrarily_close line 209