OAI/NumberTheory/CubicMoment/Estimates/DilatedNoncubeSieve.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed dilation of the coefficient support changes the three sieve constants, while preserving their common conductor exponents.

  1. lemma OAI.CubicFirstMoment.cubic_sieve_fixed_dilation line 11
  2. lemma OAI.CubicFirstMoment.ordinary_sieve_fixed_dilation line 29
  3. theorem OAI.CubicFirstMoment.dilated_noncube_three_sieve_bounds line 45