OAI/Combinatorics/Progressions/Estimates/ProgressionPartitionComposition.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.truncatedProgressionLength line 11
  2. theorem OAI.Erdos3.lt_truncatedProgressionLength_iff line 14
  3. def OAI.Erdos3.progressionBlockLabel line 24
  4. def OAI.Erdos3.progressionBlockStart line 30
  5. theorem OAI.Erdos3.progressionBlock_reconstruct line 33
  6. theorem OAI.Erdos3.progressionBlockLabel_of_point line 41
  7. theorem OAI.Erdos3.progressionBlockLabel_eq_iff line 54
  8. def OAI.Erdos3.progressionBlockEquiv line 73
  9. theorem OAI.Erdos3.progressionBlock_card line 96
  10. theorem OAI.Erdos3.progressionBlock_expect line 103
  11. theorem OAI.Erdos3.progressionBlock_label_count line 119
  12. theorem OAI.Erdos3.progressionBlock_label_count_mul line 126
  13. theorem OAI.Erdos3.progressionBlock_label_count_mul_le_twice line 133
  14. structure OAI.Erdos3.FiniteProgressionPartition line 148
  15. def OAI.Erdos3.FiniteProgressionPartition.point line 164
  16. theorem OAI.Erdos3.FiniteProgressionPartition.point_val line 166
  17. theorem OAI.Erdos3.FiniteProgressionPartition.point_lt line 169
  18. def OAI.Erdos3.FiniteProgressionPartition.cell line 173
  19. def OAI.Erdos3.FiniteProgressionPartition.offset line 175
  20. theorem OAI.Erdos3.FiniteProgressionPartition.cell_point line 177
  21. theorem OAI.Erdos3.FiniteProgressionPartition.point_cell_offset line 180
  22. def OAI.Erdos3.FiniteProgressionPartition.pointEquiv line 183
  23. theorem OAI.Erdos3.FiniteProgressionPartition.card_cell line 201
  24. theorem OAI.Erdos3.FiniteProgressionPartition.expect_cell line 204
  25. def OAI.Erdos3.FiniteProgressionPartition.whole line 217
  26. def OAI.Erdos3.FiniteProgressionPartition.blocks line 231
  27. def OAI.Erdos3.mergedIntervalLength line 253
  28. theorem OAI.Erdos3.mergedInterval_start_le line 256
  29. theorem OAI.Erdos3.mergedInterval_length_bounds line 260
  30. theorem OAI.Erdos3.mergedInterval_point_lt line 274
  31. theorem OAI.Erdos3.mergedInterval_index_unique line 285
  32. theorem OAI.Erdos3.exists_mergedInterval_coordinate line 300
  33. theorem OAI.Erdos3.truncatedProgressionLength_le line 333
  34. def OAI.Erdos3.FiniteProgressionPartition.restrict line 344
  35. theorem OAI.Erdos3.FiniteProgressionPartition.restrict_length_le line 384
  36. theorem OAI.Erdos3.FiniteProgressionPartition.restrict_start line 387
  37. theorem OAI.Erdos3.FiniteProgressionPartition.restrict_step line 390
  38. theorem OAI.Erdos3.FiniteProgressionPartition.restrict_card line 393
  39. def OAI.Erdos3.FiniteProgressionPartition.mergedIntervals line 405
  40. theorem OAI.Erdos3.FiniteProgressionPartition.mergedIntervals_length_bounds line 432
  41. theorem OAI.Erdos3.FiniteProgressionPartition.mergedIntervals_start line 438
  42. theorem OAI.Erdos3.FiniteProgressionPartition.mergedIntervals_step line 442
  43. theorem OAI.Erdos3.FiniteProgressionPartition.mergedIntervals_card line 446
  44. theorem OAI.Erdos3.FiniteProgressionPartition.cell_eq_iff_of_step_one line 449
  45. theorem OAI.Erdos3.FiniteProgressionPartition.end_le_of_step_one line 468
  46. def OAI.Erdos3.FiniteProgressionPartition.bind line 485
  47. theorem OAI.Erdos3.FiniteProgressionPartition.bind_start line 501
  48. theorem OAI.Erdos3.FiniteProgressionPartition.bind_step line 505
  49. theorem OAI.Erdos3.FiniteProgressionPartition.bind_length line 509
  50. theorem OAI.Erdos3.FiniteProgressionPartition.bind_card line 512
  51. theorem OAI.Erdos3.FiniteProgressionPartition.bind_card_mul_le line 515