OAI/Combinatorics/IndependentSets/Repetition/Reveal.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Repetition.revealEndpoint line 13
  2. def OAI.IndependentSetsGames.Foundations.Repetition.revealLaw line 16
  3. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealLaw_weight line 21
  4. def OAI.IndependentSetsGames.Foundations.Repetition.revealFirstLaw line 31
  5. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealFirstLaw_weight line 36
  6. def OAI.IndependentSetsGames.Foundations.Repetition.revealFallback line 40
  7. def OAI.IndependentSetsGames.Foundations.Repetition.revealProfile line 46
  8. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealProfile_inl_support line 50
  9. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealProfile_inr_support line 62
  10. def OAI.IndependentSetsGames.Foundations.Repetition.revealInputLaw line 74
  11. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealInputLaw_weight line 77
  12. theorem OAI.IndependentSetsGames.Foundations.Repetition.reveal_profile_recombination line 83
  13. theorem OAI.IndependentSetsGames.Foundations.Repetition.reveal_profile_inl_recombination line 90
  14. theorem OAI.IndependentSetsGames.Foundations.Repetition.reveal_profile_inr_recombination line 97
  15. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealInputLaw_inl line 104
  16. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealInputLaw_inr line 112
  17. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealProfile_inl_diagonal line 119
  18. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealProfile_inr_diagonal line 141
  19. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealLaw_sum_left line 167
  20. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealLaw_sum_right line 172
  21. theorem OAI.IndependentSetsGames.Foundations.Repetition.revealLaw_forget line 177
  22. theorem OAI.IndependentSetsGames.Foundations.Repetition.reveal_product_factorization line 186
  23. theorem OAI.IndependentSetsGames.Foundations.Repetition.reveal_product_forget line 196
  24. theorem OAI.IndependentSetsGames.Foundations.Repetition.reveal_product_expectation line 213