OAI/Computability/VertexCover/Repetition/Reveal.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.Repetition.revealEndpoint line 47
  2. def OAI.UniqueGames.Foundations.Repetition.revealLaw line 50
  3. theorem OAI.UniqueGames.Foundations.Repetition.revealLaw_weight line 55
  4. def OAI.UniqueGames.Foundations.Repetition.revealFirstLaw line 65
  5. theorem OAI.UniqueGames.Foundations.Repetition.revealFirstLaw_weight line 70
  6. def OAI.UniqueGames.Foundations.Repetition.revealFallback line 74
  7. def OAI.UniqueGames.Foundations.Repetition.revealProfile line 80
  8. theorem OAI.UniqueGames.Foundations.Repetition.revealProfile_inl_support line 84
  9. theorem OAI.UniqueGames.Foundations.Repetition.revealProfile_inr_support line 96
  10. def OAI.UniqueGames.Foundations.Repetition.revealInputLaw line 108
  11. theorem OAI.UniqueGames.Foundations.Repetition.revealInputLaw_weight line 111
  12. theorem OAI.UniqueGames.Foundations.Repetition.reveal_profile_recombination line 117
  13. theorem OAI.UniqueGames.Foundations.Repetition.reveal_profile_inl_recombination line 124
  14. theorem OAI.UniqueGames.Foundations.Repetition.reveal_profile_inr_recombination line 131
  15. theorem OAI.UniqueGames.Foundations.Repetition.revealInputLaw_inl line 138
  16. theorem OAI.UniqueGames.Foundations.Repetition.revealInputLaw_inr line 146
  17. theorem OAI.UniqueGames.Foundations.Repetition.revealProfile_inl_diagonal line 152
  18. theorem OAI.UniqueGames.Foundations.Repetition.revealProfile_inr_diagonal line 174
  19. theorem OAI.UniqueGames.Foundations.Repetition.revealLaw_sum_left line 200
  20. theorem OAI.UniqueGames.Foundations.Repetition.revealLaw_sum_right line 205
  21. theorem OAI.UniqueGames.Foundations.Repetition.revealLaw_forget line 210
  22. theorem OAI.UniqueGames.Foundations.Repetition.reveal_product_factorization line 218
  23. theorem OAI.UniqueGames.Foundations.Repetition.reveal_product_forget line 228
  24. theorem OAI.UniqueGames.Foundations.Repetition.reveal_product_expectation line 245