OAI/Computability/UniqueGames/Foundations/SharedProfiles.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

A single finite rectangle proposal law for two finite families of distributions. The subdivision includes every density appearing in either family. Consequently the local samplers share a seed space independently of their particular inputs.

  1. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.profileThresholds line 21
  2. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.mem_profileThresholds line 26
  3. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.distribution_weight_le_one line 31
  4. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sharedProfileThresholds line 40
  5. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.left_mem_sharedProfileThresholds line 44
  6. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.right_mem_sharedProfileThresholds line 49
  7. abbrev OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.SharedProfileSeed line 54
  8. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sharedProfileLeft line 58
  9. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sharedProfileRight line 62
  10. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sharedProfileReject line 66
  11. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.uniformRejectionRate line 71
  12. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.uniformRejectionRate_nonnegative line 74
  13. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.uniformRejectionRate_lt_one line 83
  14. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sharedProfileReject_nonnegative line 91
  15. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sharedProfile_reject_le_rate line 97
  16. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.nonnegative_powers_mono line 129
  17. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sharedProfile_label_diagonal_bound line 138
  18. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.exists_uniformRejectionRate_pow_lt line 172