OAI/Computability/UniqueGames/Games/MaskedVariation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Exact variation decomposition for the two choices of revealed endpoint. The support of the actual reveal profiles makes both branch identities valid, including zero-probability revealed endpoints.

  1. def OAI.UniqueGamesTheorem.Foundations.Repetition.maskedJoint line 17
  2. def OAI.UniqueGamesTheorem.Foundations.Repetition.maskedModel line 21
  3. def OAI.UniqueGamesTheorem.Foundations.Repetition.leftRevealModel line 25
  4. def OAI.UniqueGamesTheorem.Foundations.Repetition.rightRevealModel line 29
  5. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.sum_maskedJoint line 33
  6. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.maskedJoint_isProbability_iff line 49
  7. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.maskedJoint_firstMarginal_inl line 71
  8. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.maskedJoint_firstMarginal_inr line 80
  9. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.abs_half_sub_half_mul line 86
  10. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.abs_masked_inl line 92
  11. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.abs_masked_inr line 106
  12. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.masked_totalVariation_identity line 119
  13. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.leftRevealModel_totalVariation_le line 160
  14. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.rightRevealModel_totalVariation_le line 167