OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeTraceExpansion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The cubed-prime trace as two explicit finite sums. Both the actual integral representatives and their Kubota phases are retained.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeTraceSection_expansion line 10
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeCubeHecke_expansion line 40