OAI/Combinatorics/ListHadwiger/SmallList.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.SmallList.rate line 8
  2. def OAI.LinearListHadwiger.SmallList.bins line 9
  3. lemma OAI.LinearListHadwiger.SmallList.rate_pos line 12
  4. lemma OAI.LinearListHadwiger.SmallList.rate_zero line 16
  5. lemma OAI.LinearListHadwiger.SmallList.rate_succ line 17
  6. lemma OAI.LinearListHadwiger.SmallList.rate_le line 21
  7. lemma OAI.LinearListHadwiger.SmallList.geometric_budget line 24
  8. lemma OAI.LinearListHadwiger.SmallList.bins_upper line 39
  9. lemma OAI.LinearListHadwiger.SmallList.bins_lower line 60
  10. lemma OAI.LinearListHadwiger.SmallList.power_two_lower line 72
  11. theorem OAI.LinearListHadwiger.SmallList.schedule_cutoff line 77
  12. theorem OAI.LinearListHadwiger.SmallList.schedule_exists line 98
  13. theorem OAI.LinearListHadwiger.SmallList.palette_tail_cutoff line 135
  14. def OAI.LinearListHadwiger.SmallList.FractionalObstruction line 179
  15. def OAI.LinearListHadwiger.SmallList.singletonModel line 183
  16. lemma OAI.LinearListHadwiger.SmallList.number_iso line 193
  17. def OAI.LinearListHadwiger.SmallList.induceImageIso line 203
  18. lemma OAI.LinearListHadwiger.SmallList.obstruction_induce line 219
  19. lemma OAI.LinearListHadwiger.SmallList.number_le_four line 232
  20. lemma OAI.LinearListHadwiger.SmallList.stable_image line 248
  21. abbrev OAI.LinearListHadwiger.SmallList.Palette line 259
  22. def OAI.LinearListHadwiger.SmallList.block line 261
  23. lemma OAI.LinearListHadwiger.SmallList.block_card line 265
  24. lemma OAI.LinearListHadwiger.SmallList.mem_block line 268
  25. def OAI.LinearListHadwiger.SmallList.eligible line 274
  26. lemma OAI.LinearListHadwiger.SmallList.occupied_card line 278
  27. def OAI.LinearListHadwiger.SmallList.blockSize line 299
  28. lemma OAI.LinearListHadwiger.SmallList.blockSize_stage line 302
  29. lemma OAI.LinearListHadwiger.SmallList.blockSize_cleanup line 305
  30. lemma OAI.LinearListHadwiger.SmallList.palette_card line 308
  31. abbrev OAI.LinearListHadwiger.SmallList.RunPalette line 316
  32. def OAI.LinearListHadwiger.SmallList.stageBin line 318
  33. def OAI.LinearListHadwiger.SmallList.binIndex line 321
  34. lemma OAI.LinearListHadwiger.SmallList.stageBin_injective line 324
  35. def OAI.LinearListHadwiger.SmallList.runBlock line 329
  36. lemma OAI.LinearListHadwiger.SmallList.runBlock_none line 333
  37. lemma OAI.LinearListHadwiger.SmallList.runBlock_some line 336
  38. lemma OAI.LinearListHadwiger.SmallList.runPalette_card line 339
  39. lemma OAI.LinearListHadwiger.SmallList.stable_extend line 345
  40. theorem OAI.LinearListHadwiger.SmallList.stage_cover_or_obstruction line 357
  41. lemma OAI.LinearListHadwiger.SmallList.occupied_image_card line 458
  42. lemma OAI.LinearListHadwiger.SmallList.finish_cover line 474
  43. theorem OAI.LinearListHadwiger.SmallList.choosable_or_fractional_obstruction line 511