OAI/NumberTheory/CubicMoment/Theta/CubicThetaExtendedAutomorphy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The reconstructed arithmetic theta section has the actual Gamma_2 multiplier. Its integer invariance follows from S,T generation.

  1. def OAI.CubicFirstMoment.cubicThetaNormalizedStabilizer line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaNormalizedSeries_modularT line 23
  3. theorem OAI.CubicFirstMoment.cubicThetaNormalizedSeries_integer line 38
  4. theorem OAI.CubicFirstMoment.cubicThetaNormalizedSeries_extended line 61