OAI/NumberTheory/CubicMoment/Estimates/PrimaryPrimeEstimateTransfer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite loss in restoring the original modulus is absorbed in the same explicit prime majorant. No new analytic estimate is needed.

  1. lemma OAI.CubicFirstMoment.angularResidueIdealChar_zero line 11
  2. lemma OAI.CubicFirstMoment.primeCancellation_log_cost line 16
  3. theorem OAI.CubicFirstMoment.primary_angular_prime_bound_of_primitive line 40
  4. lemma OAI.CubicFirstMoment.residue_primeChebyshev_eq_ideal line 64