OAI/Computability/MinUncut/Games/LabelBound.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.CorrelatedSampling.localSample line 12
  2. def OAI.MinUncutGames.Foundations.CorrelatedSampling.localDiagonal line 16
  3. def OAI.MinUncutGames.Foundations.CorrelatedSampling.goodLabel line 21
  4. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.common_first_label_lower line 25
  5. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.finite_label_diagonal_bound line 54
  6. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.rectangle_label_diagonal_bound line 68
  7. def OAI.MinUncutGames.Foundations.CorrelatedSampling.profileThresholds line 106
  8. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.mem_profileThresholds line 111
  9. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.distribution_weight_le_one line 116
  10. def OAI.MinUncutGames.Foundations.CorrelatedSampling.sharedProfileThresholds line 125
  11. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.left_mem_sharedProfileThresholds line 129
  12. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.right_mem_sharedProfileThresholds line 134
  13. abbrev OAI.MinUncutGames.Foundations.CorrelatedSampling.SharedProfileSeed line 139
  14. def OAI.MinUncutGames.Foundations.CorrelatedSampling.sharedProfileLeft line 143
  15. def OAI.MinUncutGames.Foundations.CorrelatedSampling.sharedProfileRight line 147
  16. def OAI.MinUncutGames.Foundations.CorrelatedSampling.sharedProfileReject line 151
  17. def OAI.MinUncutGames.Foundations.CorrelatedSampling.uniformRejectionRate line 156
  18. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.uniformRejectionRate_nonnegative line 159
  19. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.uniformRejectionRate_lt_one line 168
  20. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.sharedProfileReject_nonnegative line 176
  21. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.sharedProfile_reject_le_rate line 182
  22. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.nonnegative_powers_mono line 214
  23. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.sharedProfile_label_diagonal_bound line 223
  24. theorem OAI.MinUncutGames.Foundations.CorrelatedSampling.exists_uniformRejectionRate_pow_lt line 257