OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamanujan.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite Ramanujan sum in the trace normalization of the actual cubic theta series. Its weight is the cube of the cubic residue character.

  1. lemma OAI.CubicFirstMoment.cubicThetaSymbol_cube_indicator line 14
  2. def OAI.CubicFirstMoment.cubicThetaRamanujan line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaRamanujan_prime line 25
  4. lemma OAI.CubicFirstMoment.cubicThetaRamanujan_one line 72
  5. lemma OAI.CubicFirstMoment.cubicThetaRamanujan_mul line 79