OAI/Combinatorics/Progressions/Geometry/BoxBlockBudget.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.expect_coordinate line 12
  2. def OAI.Erdos3.coordinateExceptional line 31
  3. theorem OAI.Erdos3.not_mem_coordinateExceptional line 36
  4. theorem OAI.Erdos3.coordinateExceptional_density_le line 41
  5. def OAI.Erdos3.BoxProgressionPartition.cell line 87
  6. def OAI.Erdos3.BoxProgressionPartition.point line 89
  7. theorem OAI.Erdos3.BoxProgressionPartition.point_val line 93
  8. theorem OAI.Erdos3.BoxProgressionPartition.cell_point line 98
  9. def OAI.Erdos3.BoxProgressionPartition.pointEquiv line 103
  10. theorem OAI.Erdos3.BoxProgressionPartition.pointEquiv_val line 109
  11. theorem OAI.Erdos3.BoxProgressionPartition.card_cell line 112
  12. theorem OAI.Erdos3.BoxProgressionPartition.expect_cell line 117
  13. def OAI.Erdos3.BoxProgressionPartition.normalizedPoint line 139
  14. def OAI.Erdos3.BoxProgressionPartition.normalizedStart line 142
  15. theorem OAI.Erdos3.BoxProgressionPartition.normalizedPoint_dist_start line 146
  16. theorem OAI.Erdos3.BoxProgressionPartition.point_residue line 163
  17. theorem OAI.Erdos3.BoxProgressionPartition.blocks_normalizedPoint_dist_start line 170
  18. theorem OAI.Erdos3.exists_partition_cell_norm_mean_le line 193
  19. theorem OAI.Erdos3.BoxProgressionPartition.expect_cell_complex line 231
  20. theorem OAI.Erdos3.BoxProgressionPartition.exists_positive_box_norm_mean_le line 242
  21. theorem OAI.Erdos3.BoxProgressionPartition.exists_box_norm_mean_le line 258
  22. theorem OAI.Erdos3.short_progression_cell_mass_le line 277
  23. theorem OAI.Erdos3.short_box_side_mass_le line 302
  24. theorem OAI.Erdos3.progressionBlock_short_side_bound line 338
  25. theorem OAI.Erdos3.boxBlock_short_side_budget line 348
  26. theorem OAI.Erdos3.exists_box_block_mesh line 370