OAI/NumberTheory/CubicMoment/Theta/CubicThetaFrequencyHolomorphic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Holomorphy of the actual arithmetic Fourier coefficients on their initial half-plane, with a common bound independent of the frequency.

  1. lemma OAI.CubicFirstMoment.cubicThetaFrequencyTerm_strip_bound line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_differentiableOn line 20
  3. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_differentiableAt line 31
  4. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_bound line 43