OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedRowConductor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The ramified row weight has conductor dividing nine times its primary part. Consequently the lambda exponent of a nonzero Fourier row is bounded by the lambda exponent of its frequency plus two. These are finite character identities, with the original zero extension retained.

  1. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_lambda_pow line 16
  2. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_lambda_periodic line 25
  3. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_ramified_periodic line 40
  4. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_ramified_support line 53
  5. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_ramified_zero line 90