OAI/Combinatorics/ListHadwiger/ColorBins.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LinearListHadwiger.ColorBins.probability_all line 11
  2. def OAI.LinearListHadwiger.ColorBins.uniform line 29
  3. lemma OAI.LinearListHadwiger.ColorBins.uniform_nonneg line 31
  4. lemma OAI.LinearListHadwiger.ColorBins.uniform_sum line 33
  5. lemma OAI.LinearListHadwiger.ColorBins.uniform_probability line 38
  6. lemma OAI.LinearListHadwiger.ColorBins.palette_miss line 48
  7. lemma OAI.LinearListHadwiger.ColorBins.palette_miss_bound line 66
  8. def OAI.LinearListHadwiger.ColorBins.occupied line 85
  9. lemma OAI.LinearListHadwiger.ColorBins.bad_block_witness line 88
  10. lemma OAI.LinearListHadwiger.ColorBins.bad_block_probability line 102
  11. theorem OAI.LinearListHadwiger.ColorBins.exists_bins_finite line 138
  12. theorem OAI.LinearListHadwiger.ColorBins.exists_bins line 175
  13. theorem OAI.LinearListHadwiger.ColorBins.listColorable_of_bin_cover line 213
  14. theorem OAI.LinearListHadwiger.Fractional.distribution line 232
  15. lemma OAI.LinearListHadwiger.Cleanup.probability_membership line 269
  16. theorem OAI.LinearListHadwiger.Cleanup.stable_cover line 276
  17. theorem OAI.LinearListHadwiger.Cleanup.cleanup_source line 326