OAI/Combinatorics/Progressions/Lattices/NaturalScaleIntegerWindow.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.centeredIntegerBox line 13
  2. theorem OAI.Erdos3.mem_centeredIntegerBox line 16
  3. theorem OAI.Erdos3.card_centeredIntegerBox line 20
  4. theorem OAI.Erdos3.card_doubled_centeredIntegerBox_le line 28
  5. theorem OAI.Erdos3.card_mul_le_of_kernel_translates line 39
  6. theorem OAI.Erdos3.kernel_eq_zero_of_dense_integer_box line 66
  7. theorem OAI.Erdos3.injOn_small_integer_box_of_dense_subset line 91
  8. theorem OAI.Erdos3.integerSites_card_le line 123
  9. theorem OAI.Erdos3.integerSites_card_le_exp line 134
  10. theorem OAI.Erdos3.injOn_shrunk_integer_box_of_distinct_points line 167
  11. theorem OAI.Erdos3.injOn_shrunk_integer_box_of_distinct_residues line 208
  12. def OAI.Erdos3.naturalScaleIntegerWindow line 235
  13. theorem OAI.Erdos3.mem_naturalScaleIntegerWindow_of_bound line 238
  14. theorem OAI.Erdos3.naturalScaleIntegerWindow_card_le line 245
  15. def OAI.Erdos3.naturalScaleProductWindow line 259
  16. theorem OAI.Erdos3.mem_naturalScaleProductWindow_iff line 264
  17. theorem OAI.Erdos3.naturalScaleProductWindow_card_le line 270