OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootDilationSection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The once-dilated global section is an actual root-cover section. It lies in the zero root-frequency space and intertwines the two Weyl actions.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeRootDilationSection line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaPrimeRootDilationSection_translate line 26
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootDilationSection_average line 43