OAI/Computability/VertexCover/Repetition/PartialReveal.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.Repetition.mergeAt line 45
  2. theorem OAI.UniqueGames.Foundations.Repetition.mergeAt_self line 49
  3. theorem OAI.UniqueGames.Foundations.Repetition.mergeAt_other line 53
  4. def OAI.UniqueGames.Foundations.Repetition.partialRevealWeight line 57
  5. theorem OAI.UniqueGames.Foundations.Repetition.product_reveal_at line 61
  6. def OAI.UniqueGames.Foundations.Repetition.partialRevealMarginal line 71
  7. def OAI.UniqueGames.Foundations.Repetition.fullRevealMarginal line 78
  8. theorem OAI.UniqueGames.Foundations.Repetition.fullRevealMarginal_merge line 87
  9. def OAI.UniqueGames.Foundations.Repetition.fullRevealModel line 113
  10. theorem OAI.UniqueGames.Foundations.Repetition.fullRevealModel_merge line 120
  11. def OAI.UniqueGames.Foundations.Repetition.revealSplitEquiv line 128
  12. theorem OAI.UniqueGames.Foundations.Repetition.totalVariation_comp_equiv line 150
  13. theorem OAI.UniqueGames.Foundations.Repetition.fullReveal_totalVariation line 158
  14. theorem OAI.UniqueGames.Foundations.Repetition.leftReveal_full_error line 173
  15. theorem OAI.UniqueGames.Foundations.Repetition.rightReveal_full_error line 182