OAI/Combinatorics/IndependentSets/Repetition/Rectangle.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.sum_div_const line 15
  2. abbrev OAI.IndependentSetsGames.Foundations.CorrelatedSampling.RectangleSeed line 19
  3. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangleWeight line 22
  4. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangleAccept line 26
  5. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangleWeight_nonnegative line 30
  6. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangleWeight_normalized line 34
  7. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangleDistribution line 45
  8. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangle_row_mass line 51
  9. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangle_acceptance_mass line 68
  10. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangle_label_mass line 78
  11. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.min_mem_thresholds line 107
  12. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.max_mem_thresholds line 111
  13. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangle_union_mass line 115
  14. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.rectangle_common_label_mass line 127
  15. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.localSample line 145
  16. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.localDiagonal line 149
  17. def OAI.IndependentSetsGames.Foundations.CorrelatedSampling.goodLabel line 154
  18. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.common_first_label_lower line 158
  19. theorem OAI.IndependentSetsGames.Foundations.CorrelatedSampling.finite_label_diagonal_bound line 187