OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeRootWeylAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The zero Fourier row of the actual Weyl action. Subtracting the zero column removes the dilation term exactly, without assuming it vanishes.

  1. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_average line 10
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_zero_row line 19
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimeRootWeyl_zero_row_difference line 33