OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspRemainder.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Quantitative cusp decay of the actual Eisenstein series after its constant Fourier mode has been removed.

  1. def OAI.CubicFirstMoment.cubicThetaFrequencyBound line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaFrequencyBound_nonneg line 17
  3. def OAI.CubicFirstMoment.cubicThetaNonzeroFrequencyTerm line 21
  4. lemma OAI.CubicFirstMoment.cubicThetaNonzeroFrequencyTerm_bound line 26
  5. lemma OAI.CubicFirstMoment.cubicThetaNonzeroFrequencyTerm_summable line 36
  6. lemma OAI.CubicFirstMoment.cubicThetaNonzeroFrequencySum_bound line 41
  7. def OAI.CubicFirstMoment.cubicThetaCuspPowerConstant line 61
  8. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_cusp_power_bound line 66