OAI/NumberTheory/CubicMoment/Theta/CubicThetaIncomingLocalFinite.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A compact positive-height set meets only finitely many incoming row supports. The bound is arithmetic and is uniform in the spectral parameter, so the resulting finite-sum identities support differentiation.

  1. theorem OAI.CubicFirstMoment.cubicThetaIncomingRows_compact line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaIncomingEisenstein_compact_sum line 40
  3. theorem OAI.CubicFirstMoment.cubicThetaIncomingEisenstein_analytic line 51