OAI/Computability/MinUncut/PCP/DistributionMaps.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.weight_eq_probability_singleton line 12
  2. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.pushforward_comp line 17
  3. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.transport_eq_pushforward line 25
  4. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.expectation_pushforward line 33
  5. theorem OAI.MinUncutGames.Foundations.Games.FiniteDistribution.pushforward_mixture line 42
  6. theorem OAI.MinUncutGames.Foundations.Repetition.isProbability_comp_equiv line 59
  7. theorem OAI.MinUncutGames.Foundations.Repetition.partialRevealMarginal_isProbability line 68
  8. abbrev OAI.MinUncutGames.Foundations.Repetition.SelectedCommonData line 89
  9. theorem OAI.MinUncutGames.Foundations.Repetition.selected_fullReveal_isProbability line 94
  10. def OAI.MinUncutGames.Foundations.Repetition.selectedCommonLaw line 111
  11. theorem OAI.MinUncutGames.Foundations.Repetition.firstMarginal_totalVariation_le line 123
  12. def OAI.MinUncutGames.Foundations.Repetition.leftCommonMarginal line 132
  13. def OAI.MinUncutGames.Foundations.Repetition.leftCommonProfile line 135
  14. def OAI.MinUncutGames.Foundations.Repetition.swapSeedLeft line 138
  15. theorem OAI.MinUncutGames.Foundations.Repetition.leftCommonMarginal_isProbability line 144
  16. theorem OAI.MinUncutGames.Foundations.Repetition.leftCommonProfile_isProbability line 149
  17. theorem OAI.MinUncutGames.Foundations.Repetition.leftCommonProfile_error line 154
  18. def OAI.MinUncutGames.Foundations.Repetition.swapQuestionEndpoints line 191
  19. def OAI.MinUncutGames.Foundations.Repetition.rightCommonMarginal line 197
  20. def OAI.MinUncutGames.Foundations.Repetition.rightCommonProfile line 200
  21. theorem OAI.MinUncutGames.Foundations.Repetition.rightCommonProfile_isProbability line 203
  22. theorem OAI.MinUncutGames.Foundations.Repetition.swap_question_pushforward_snd line 209
  23. theorem OAI.MinUncutGames.Foundations.Repetition.leftRevealModel_swap line 215
  24. theorem OAI.MinUncutGames.Foundations.Repetition.rightCommonProfile_error line 225