OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedPrimarySupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Away from lambda, the literal frequency series is supported on the two signed primary classes. This is a finite ramified selection rule.

  1. lemma OAI.CubicFirstMoment.unit_ramified_primary_congruence line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_primary_support line 25
  3. theorem OAI.CubicFirstMoment.cubicThetaFrequencyDirichlet_primary_support line 58