OAI/NumberTheory/CubicMoment/Estimates/PrimitiveAngularPrimeEstimate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The sharp angular prime-ideal estimate is derived from the actual primitive completions. The square uses its own conductor and finite Euler correction.

  1. lemma OAI.CubicFirstMoment.primeSetExponent_support_norm_le line 12
  2. lemma OAI.CubicFirstMoment.angularResidueIdealChar_at_zero line 20
  3. theorem OAI.CubicFirstMoment.primitive_angular_prime_ideal_estimate line 24