OAI/NumberTheory/CubicMoment/Theta/CubicThetaFiniteCuspEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact summation of the sharp cusp estimates. Distinct cusp classes are disjoint already at height one, so no covering multiplicity is lost in the gradient coefficient.

  1. lemma OAI.CubicFirstMoment.cubicThetaIntegral_cover_le line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaFiniteCusps_energy_le line 33
  3. lemma OAI.CubicFirstMoment.cubicThetaFiniteCusps_mass_le line 44