OAI/Combinatorics/IndependentSets/Repetition/Rectangle2.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangle_label_diagonal_bound line 15
  2. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.profileThresholds line 51
  3. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.mem_profileThresholds line 56
  4. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.distribution_weight_le_one line 61
  5. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sharedProfileThresholds line 70
  6. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.left_mem_sharedProfileThresholds line 74
  7. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.right_mem_sharedProfileThresholds line 79
  8. abbrev OAI.IndependentSetsGames.Foundations.CorrelatedSampling.SharedProfileSeed line 84
  9. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sharedProfileLeft line 88
  10. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sharedProfileRight line 92
  11. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sharedProfileReject line 96
  12. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.uniformRejectionRate line 101
  13. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.uniformRejectionRate_nonnegative line 104
  14. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.uniformRejectionRate_lt_one line 113
  15. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sharedProfileReject_nonnegative line 121
  16. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sharedProfile_reject_le_rate line 127
  17. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.nonnegative_powers_mono line 159
  18. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sharedProfile_label_diagonal_bound line 168
  19. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.exists_uniformRejectionRate_pow_lt line 202