OAI/Computability/UniqueGames/Foundations/MixtureLemmas.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite shared randomness is an actual convex mixture of distributions.

  1. def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.mixture line 17
  2. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_mixture line 27
  3. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_mixture_le line 44
  4. def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.totalVariation line 71
  5. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.totalVariation_nonnegative line 74
  6. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.totalVariation_comm line 78
  7. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_sub_le_totalVariation line 89

    Source documentation

    A one-sided event difference is bounded by half the total absolute mass difference. Normalization is used; the full absolute-mass sum would lose a factor of two needed in the repetition argument.

    theorem probability_sub_le_totalVariation (μ ν : FiniteDistribution Ω)
    (event : Ω → Bool) :
    μ.probability event - ν.probability event ≤ μ.totalVariation ν := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution

  8. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_abs_sub_le_totalVariation line 105
  9. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_le_add_totalVariation line 115