OAI/NumberTheory/CubicMoment/Estimates/FullPrimeMellinEnvelope.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A polynomial coarse envelope for the unchanged full prime rows, uniform in Mellin height and the ambient set of prime divisors.

  1. lemma OAI.CubicFirstMoment.fullPrimeSupport_card_bound line 15
  2. lemma OAI.CubicFirstMoment.fullPrimeCoefficient_l1_square line 24
  3. theorem OAI.CubicFirstMoment.logarithmic_full_mellin_envelope line 39