OAI/NumberTheory/CubicMoment/Theta/CubicThetaConstantModeResidue.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact residue of the zero Fourier mode of the principal level-three Eisenstein series. Nonzero Fourier modes remain separate.

  1. def OAI.CubicFirstMoment.cubicThetaConstantModeContinuation line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaConstantModeContinuation_right line 16
  3. lemma OAI.CubicFirstMoment.cubicTheta_principalZeta_residue_value line 22
  4. theorem OAI.CubicFirstMoment.cubicThetaConstantModeContinuation_residue line 32