OAI/NumberTheory/CubicGauss/SmoothBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Smoothed sieve inequalities and dyadic coefficient bins.

  1. lemma OAI.CubicFirstMoment.cubicRowEnergy_card_bound line 15
  2. lemma OAI.CubicFirstMoment.cubicRowEnergy_gaussian_summable line 30
  3. lemma OAI.CubicFirstMoment.cubic_gaussian_norm_eq line 39
  4. lemma OAI.CubicFirstMoment.cubic_cutoff_le_gaussian line 53
  5. lemma OAI.CubicFirstMoment.initial_positive_factor line 78
  6. theorem OAI.CubicFirstMoment.cubic_sieve_thin_initial line 114
  7. def OAI.CubicFirstMoment.sieveBin line 160
  8. lemma OAI.CubicFirstMoment.sieveBin_range line 163
  9. lemma OAI.CubicFirstMoment.sieveBin_unique line 176
  10. lemma OAI.CubicFirstMoment.sieveBin_sum line 187
  11. lemma OAI.CubicFirstMoment.sieveBin_subset line 204
  12. lemma OAI.CubicFirstMoment.sieveBin_thin line 212
  13. lemma OAI.CubicFirstMoment.sieveBin_top line 218
  14. lemma OAI.CubicFirstMoment.sieveBin_count_power line 225
  15. lemma OAI.CubicFirstMoment.cubic_bin_operator_bound line 246
  16. theorem OAI.CubicFirstMoment.cubic_thin_to_full line 273