OAI/Computability/VertexCover/Games/KernelSampling.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.pushforward_eq_of_agree_on_support line 46
  2. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.product_pushforward line 61
  3. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.table_row_weight_ne_zero line 78
  4. theorem OAI.UniqueGames.Foundations.Games.FiniteDistribution.table_repair_pushforward line 88
  5. abbrev OAI.UniqueGames.Foundations.Games.KernelSampling.Seed line 105
  6. def OAI.UniqueGames.Foundations.Games.KernelSampling.readLeft line 107
  7. def OAI.UniqueGames.Foundations.Games.KernelSampling.readRight line 108
  8. def OAI.UniqueGames.Foundations.Games.KernelSampling.seedLaw line 110
  9. theorem OAI.UniqueGames.Foundations.Games.KernelSampling.read_joint_pushforward line 117
  10. theorem OAI.UniqueGames.Foundations.Games.KernelSampling.repaired_joint_pushforward line 130
  11. def OAI.UniqueGames.Foundations.Games.KernelSampling.completedLeft line 152
  12. def OAI.UniqueGames.Foundations.Games.KernelSampling.completedRight line 156
  13. theorem OAI.UniqueGames.Foundations.Games.KernelSampling.completedLeft_coordinate line 160
  14. theorem OAI.UniqueGames.Foundations.Games.KernelSampling.completedRight_coordinate line 164
  15. theorem OAI.UniqueGames.Foundations.Games.KernelSampling.update_eq_of_coordinate line 168
  16. theorem OAI.UniqueGames.Foundations.Games.KernelSampling.completed_joint_pushforward line 173