OAI/NumberTheory/CubicMoment/Theta/CubicThetaInvertedFrequencyBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Absolute arithmetic and heat majorants for collecting the actual inverted Fourier coefficients on their half-plane of convergence.

  1. def OAI.CubicFirstMoment.cubicThetaInvertedFrequencyTerm line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaInvertedFrequencyDirichlet_tsum line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaInvertedFrequencyDirichlet_zero line 31
  4. lemma OAI.CubicFirstMoment.cubicThetaInvertedGaussCoefficient_norm_real line 40
  5. lemma OAI.CubicFirstMoment.cubicThetaInvertedFrequencyTerm_bound line 45
  6. lemma OAI.CubicFirstMoment.cubicThetaInvertedFrequencyTerm_norm_summable line 70
  7. lemma OAI.CubicFirstMoment.cubicThetaInvertedFrequency_heat_norm_summable line 75