OAI/NumberTheory/CubicMoment/Theta/CubicThetaHighCuspRows.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

In a high cusp, the incoming term cancels precisely the constant rows. The remaining literal terms are smooth primitive height powers.

  1. def OAI.CubicFirstMoment.cubicThetaHighCuspRow line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaHighCuspRow_eq line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaHighCuspRow_contDiffAt line 37
  4. lemma OAI.CubicFirstMoment.cubicThetaHighCuspRow_fderiv_bound line 46