OAI/Computability/VertexCover/Repetition/MaskedVariation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.Repetition.maskedJoint line 45
  2. def OAI.UniqueGames.Foundations.Repetition.maskedModel line 49
  3. def OAI.UniqueGames.Foundations.Repetition.leftRevealModel line 53
  4. def OAI.UniqueGames.Foundations.Repetition.rightRevealModel line 57
  5. theorem OAI.UniqueGames.Foundations.Repetition.sum_maskedJoint line 61
  6. theorem OAI.UniqueGames.Foundations.Repetition.maskedJoint_isProbability_iff line 77
  7. theorem OAI.UniqueGames.Foundations.Repetition.maskedJoint_firstMarginal_inl line 99
  8. theorem OAI.UniqueGames.Foundations.Repetition.maskedJoint_firstMarginal_inr line 108
  9. theorem OAI.UniqueGames.Foundations.Repetition.abs_half_sub_half_mul line 114
  10. theorem OAI.UniqueGames.Foundations.Repetition.abs_masked_inl line 120
  11. theorem OAI.UniqueGames.Foundations.Repetition.abs_masked_inr line 134
  12. theorem OAI.UniqueGames.Foundations.Repetition.masked_totalVariation_identity line 147
  13. theorem OAI.UniqueGames.Foundations.Repetition.leftRevealModel_totalVariation_le line 188
  14. theorem OAI.UniqueGames.Foundations.Repetition.rightRevealModel_totalVariation_le line 195