OAI/Combinatorics/Progressions/Lattices/ShortIntegerCubeBudget.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.natCeil_le_exp_succ line 10
  2. theorem OAI.Erdos3.natFinsetSup_cast_le line 15
  3. theorem OAI.Erdos3.integerPolynomialInitialScale_exp_bound line 21
  4. theorem OAI.Erdos3.principalSamplingGapRatio_exp_bound line 37
  5. theorem OAI.Erdos3.commonPolynomialGapRatio_exp_bound line 53
  6. theorem OAI.Erdos3.commonPolynomialInitialScale_exp_bound line 63
  7. def OAI.Erdos3.integerAxisShortBound line 82
  8. theorem OAI.Erdos3.integerAxisSideLength_inactive_of_short line 85
  9. theorem OAI.Erdos3.integerAxisSideLength_short_scale line 95
  10. theorem OAI.Erdos3.integerAxisSideLength_long_or_bounded line 113
  11. theorem OAI.Erdos3.inactiveDenominator_le_exp line 120
  12. theorem OAI.Erdos3.integerAxisShortBound_le_exp line 127
  13. theorem OAI.Erdos3.integerAxisPrincipalPMF_pure_of_short line 141
  14. def OAI.Erdos3.shortIntegerImageAxis line 160
  15. theorem OAI.Erdos3.shortIntegerImageAxis_exact line 169
  16. theorem OAI.Erdos3.shortIntegerImageAllowance_le_exp line 179
  17. theorem OAI.Erdos3.shortIntegerImageAxis_log_bounds line 198
  18. theorem OAI.Erdos3.shortIntegerAxis_block_volume line 232
  19. def OAI.Erdos3.shortIntegerCubeFourierAxis line 252
  20. theorem OAI.Erdos3.shortIntegerCubeFourierAxis_exact line 267
  21. theorem OAI.Erdos3.shortIntegerCubeRadius_le_exp line 291
  22. def OAI.Erdos3.shortIntegerFourierLog line 316
  23. theorem OAI.Erdos3.shortIntegerFourierAllowance_le_exp line 319
  24. theorem OAI.Erdos3.shortIntegerCubeFourierAxis_log_bounds line 342