OAI/NumberTheory/CubicMoment/Theta/CubicThetaRegularizedFourier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A single holomorphic representative of the pole-cleared arithmetic Fourier coefficient on Re(s)>1, including its actual residue value.

  1. lemma OAI.CubicFirstMoment.regularized_analytic line 12
  2. def OAI.CubicFirstMoment.cubicThetaRegularizedFrequency line 22
  3. lemma OAI.CubicFirstMoment.cubicThetaClearedFrequency_meromorphic line 25
  4. theorem OAI.CubicFirstMoment.cubicThetaRegularizedFrequency_analytic line 31
  5. theorem OAI.CubicFirstMoment.cubicThetaRegularizedFrequency_germ line 47
  6. theorem OAI.CubicFirstMoment.cubicThetaRegularizedFrequency_residue line 53