OAI/Computability/UniqueGames/Foundations/Rectangle.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

An actual finite probability rectangle implementing all thresholds from a fixed finite list. The seed distribution is shared; each local acceptance test depends only on its own density.

  1. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sum_div_const line 17
  2. abbrev OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.RectangleSeed line 21
  3. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangleWeight line 24
  4. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangleAccept line 28
  5. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangleWeight_nonnegative line 32
  6. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangleWeight_normalized line 36
  7. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangleDistribution line 47
  8. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangle_row_mass line 53
  9. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangle_acceptance_mass line 70
  10. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangle_label_mass line 80
  11. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.min_mem_thresholds line 109
  12. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.max_mem_thresholds line 113
  13. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangle_union_mass line 117
  14. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.rectangle_common_label_mass line 129