OAI/NumberTheory/CubicMoment/Theta/CubicThetaHorizontalFourierVanishing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Dilation kills precisely the horizontal frequencies outside the corresponding principal ideal, by the primitive finite trace pairing.

  1. lemma OAI.CubicFirstMoment.cubicThetaHorizontalCharacter_fraction line 13
  2. theorem OAI.CubicFirstMoment.cubicThetaHorizontalFourier_dilate_zero line 24