OAI/Computability/MinUncut/PCP/Completion.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Repetition.normalizeOr line 15
  2. theorem OAI.MinUncutGames.Foundations.Repetition.sum_mul_normalizeOr line 23
  3. theorem OAI.MinUncutGames.Foundations.Repetition.local_completion_recombination line 38
  4. theorem OAI.MinUncutGames.Foundations.Repetition.factorized_completion_row line 51
  5. def OAI.MinUncutGames.Foundations.Repetition.revealEndpoint line 76
  6. def OAI.MinUncutGames.Foundations.Repetition.revealLaw line 79
  7. theorem OAI.MinUncutGames.Foundations.Repetition.revealLaw_weight line 84
  8. def OAI.MinUncutGames.Foundations.Repetition.revealFirstLaw line 94
  9. theorem OAI.MinUncutGames.Foundations.Repetition.revealFirstLaw_weight line 99
  10. def OAI.MinUncutGames.Foundations.Repetition.revealFallback line 103
  11. def OAI.MinUncutGames.Foundations.Repetition.revealProfile line 109
  12. theorem OAI.MinUncutGames.Foundations.Repetition.revealProfile_inl_support line 113
  13. theorem OAI.MinUncutGames.Foundations.Repetition.revealProfile_inr_support line 125
  14. def OAI.MinUncutGames.Foundations.Repetition.revealInputLaw line 137
  15. theorem OAI.MinUncutGames.Foundations.Repetition.revealInputLaw_weight line 140
  16. theorem OAI.MinUncutGames.Foundations.Repetition.reveal_profile_recombination line 146
  17. theorem OAI.MinUncutGames.Foundations.Repetition.reveal_profile_inl_recombination line 153
  18. theorem OAI.MinUncutGames.Foundations.Repetition.reveal_profile_inr_recombination line 160
  19. theorem OAI.MinUncutGames.Foundations.Repetition.revealInputLaw_inl line 167
  20. theorem OAI.MinUncutGames.Foundations.Repetition.revealInputLaw_inr line 175
  21. theorem OAI.MinUncutGames.Foundations.Repetition.revealProfile_inl_diagonal line 182
  22. theorem OAI.MinUncutGames.Foundations.Repetition.revealProfile_inr_diagonal line 204
  23. theorem OAI.MinUncutGames.Foundations.Repetition.revealLaw_sum_left line 230
  24. theorem OAI.MinUncutGames.Foundations.Repetition.revealLaw_sum_right line 235
  25. theorem OAI.MinUncutGames.Foundations.Repetition.revealLaw_forget line 240
  26. theorem OAI.MinUncutGames.Foundations.Repetition.reveal_product_factorization line 249
  27. theorem OAI.MinUncutGames.Foundations.Repetition.reveal_product_forget line 259
  28. theorem OAI.MinUncutGames.Foundations.Repetition.reveal_product_expectation line 276