OAI/NumberTheory/CubicMoment/Theta/CubicThetaFirstPair.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The first two literal arithmetic Fourier terms have a uniformly negative contribution at height one.

  1. lemma OAI.CubicFirstMoment.cubicThetaFrequency_lambda line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient_lambda line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaFrequency_neg_norm line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaFirstPair_real_bound line 25