OAI/Combinatorics/Progressions/Estimates/DenseProgressionInnerFamily.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.balanced_product_side_power line 13
  2. theorem OAI.Erdos3.side_power_after_width_loss line 23
  3. theorem OAI.Erdos3.moderate_coefficient_side_power line 31
  4. theorem OAI.Erdos3.log_scale_range_power line 46
  5. theorem OAI.Erdos3.exists_minimum_side_power line 51
  6. theorem OAI.Erdos3.scaled_grid_volume_bound line 58
  7. theorem OAI.Erdos3.card_integerProgressionSupport line 71
  8. theorem OAI.Erdos3.integerProgressionSupport_point line 80
  9. theorem OAI.Erdos3.progression_endpoint_bounds line 92
  10. theorem OAI.Erdos3.progression_slice_geometry line 119
  11. theorem OAI.Erdos3.integerProgressionSupport_reindex line 142
  12. theorem OAI.Erdos3.exists_bounded_progression_reindex line 156
  13. theorem OAI.Erdos3.progressionFamily_geometric_bounds line 213
  14. theorem OAI.Erdos3.progression_slice_endpoint_geometry line 256
  15. theorem OAI.Erdos3.progression_slice_step_le_inverse_density line 291
  16. theorem OAI.Erdos3.progression_slice_stride_period_le_exp line 310
  17. theorem OAI.Erdos3.progression_endpoint_index_error line 328
  18. theorem OAI.Erdos3.progression_slice_endpoint_evaluation line 344
  19. theorem OAI.Erdos3.integerProgressionSupport_singleton line 360
  20. theorem OAI.Erdos3.exists_same_stride_progression_reindex line 368
  21. theorem OAI.Erdos3.exists_bounded_common_stride_reindex line 393
  22. theorem OAI.Erdos3.exists_dense_progression_inner_family line 432