OAI/Computability/MinUncut/PCP/ProfileCorrection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal line 13
  2. theorem OAI.MinUncutGames.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal_isProbability line 16
  3. theorem OAI.MinUncutGames.Foundations.Repetition.ProfileCorrection.seedQuestionMarginal_first line 27
  4. theorem OAI.MinUncutGames.Foundations.Repetition.ProfileCorrection.totalVariation_triangle line 32
  5. theorem OAI.MinUncutGames.Foundations.Repetition.ProfileCorrection.left_profile_correction line 41
  6. def OAI.MinUncutGames.Foundations.Repetition.revealedProductWeight line 98
  7. def OAI.MinUncutGames.Foundations.Repetition.revealedLeftWeight line 104
  8. def OAI.MinUncutGames.Foundations.Repetition.revealedRightWeight line 109
  9. theorem OAI.MinUncutGames.Foundations.Repetition.revealedProductWeight_factorizes line 114
  10. theorem OAI.MinUncutGames.Foundations.Repetition.revealedProductWeight_local_restrictions line 127
  11. theorem OAI.MinUncutGames.Foundations.Repetition.productWeight_mass line 140
  12. def OAI.MinUncutGames.Foundations.Repetition.normalizedWeight line 146
  13. theorem OAI.MinUncutGames.Foundations.Repetition.normalizedWeight_isProbability line 149
  14. theorem OAI.MinUncutGames.Foundations.Repetition.normalized_productWeight line 157
  15. theorem OAI.MinUncutGames.Foundations.Repetition.normalized_rectangle_restriction line 165