OAI/NumberTheory/CubicMoment/Estimates/SupportedIdealCount.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A Rankin bound for ideals supported on a varying small modulus. The finite Euler product is controlled by an arbitrarily small modulus power.

  1. lemma OAI.CubicFirstMoment.idealExponentNorm_prod_of_support_subset line 12
  2. lemma OAI.CubicFirstMoment.supported_norm_rpow line 20
  3. lemma OAI.CubicFirstMoment.finite_geometric_code_sum line 34
  4. lemma OAI.CubicFirstMoment.ideal_supported_rankin_sum line 57