OAI/NumberTheory/CubicMoment/Theta/CubicThetaIncomingCompactIntegral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The compact strip contribution of the incoming arithmetic series is entire in the spectral parameter. It contributes no pole to Fourier tests.

  1. lemma OAI.CubicFirstMoment.cubicThetaIncomingTerm_point_continuous line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaRowLogHeight_point_continuous line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaIncomingTerm_exponential line 27
  4. lemma OAI.CubicFirstMoment.cubicThetaIncomingCompactIntegral_differentiable line 36