OAI/NumberTheory/CubicMoment/Theta/CubicThetaExtendedMultiplier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The cubic multiplier on Gamma_2. Its value is independent of the principal/integer factorization, and it is trivial on SL(2,Z).

  1. lemma OAI.CubicFirstMoment.cubicThetaKubota_factorization_independent line 11
  2. def OAI.CubicFirstMoment.cubicThetaExtendedValue line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaExtendedValue_of_decomposition line 26
  4. theorem OAI.CubicFirstMoment.cubicThetaExtendedValue_mul line 33
  5. def OAI.CubicFirstMoment.cubicThetaExtendedCharacter line 50
  6. theorem OAI.CubicFirstMoment.cubicThetaExtendedValue_principal line 57
  7. theorem OAI.CubicFirstMoment.cubicThetaExtendedValue_integer line 61
  8. lemma OAI.CubicFirstMoment.cubicThetaExtendedValue_norm line 66
  9. lemma OAI.CubicFirstMoment.cubicThetaExtendedCharacter_cube line 69