OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompactCuspSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A compact smooth automorphic section vanishes uniformly high in every arithmetic cusp. This is derived from its actual quotient support, not imposed as a separate cusp-decay hypothesis.

  1. lemma OAI.CubicFirstMoment.cubicThetaSmoothTests_cusp_support line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaSmoothTests_cusp_function_support line 30