OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The centered prime comparison from the constructed arithmetic theta transform, the actual low-height bounds and the actual high-height tails. No published analytic input is retained as a hypothesis.

  1. lemma OAI.CubicFirstMoment.cubicTheta_primeProductLowHeight_isLittleO line 14
  2. lemma OAI.CubicFirstMoment.cubicTheta_primeComparison line 48