OAI/NumberTheory/CubicMoment/Estimates/MellinEnvelopeBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The coarse Mellin envelope costs only the bounded number of prime factors in a coefficient, not the size of the ambient set of primes.

  1. lemma OAI.CubicFirstMoment.divisor_subset_l1_square line 13
  2. theorem OAI.CubicFirstMoment.coprimeMellinEnvelope_of_divisor_count line 44
  3. theorem OAI.CubicFirstMoment.fullPrime_coprimeMellinEnvelope line 65