OAI/Combinatorics/IndependentSets/Repetition/Mixture.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.mixture line 16
  2. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_mixture line 26
  3. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.probability_mixture_le line 43
  4. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.weight_eq_probability_singleton line 59
  5. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.pushforward_comp line 64
  6. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.transport_eq_pushforward line 72
  7. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.expectation_pushforward line 80
  8. theorem OAI.IndependentSetsGames.Foundations.Games.FiniteDistribution.pushforward_mixture line 89
  9. theorem OAI.IndependentSetsGames.Foundations.Repetition.isProbability_comp_equiv line 103
  10. theorem OAI.IndependentSetsGames.Foundations.Repetition.partialRevealMarginal_isProbability line 112
  11. abbrev OAI.IndependentSetsGames.Foundations.Repetition.SelectedCommonData line 133
  12. theorem OAI.IndependentSetsGames.Foundations.Repetition.selected_fullReveal_isProbability line 138
  13. def OAI.IndependentSetsGames.Foundations.Repetition.selectedCommonLaw line 155