OAI/NumberTheory/CubicMoment/Theta/CubicThetaHighCuspDifferentiation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Differentiate the exact high-cusp expansion of the arithmetic remainder. The derivative bound is obtained from a summable majorant.

  1. lemma OAI.CubicFirstMoment.cubicThetaHighCuspRow_sum line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaHighCuspRow_sum_summable line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaHighCusp_fderiv_eq line 28
  4. theorem OAI.CubicFirstMoment.cubicThetaArithmeticCusp_fderiv_bound line 51