OAI/NumberTheory/CubicMoment/Theta/CubicThetaInvertedFourierObservable.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Nonzero Fourier observations at the inverted cusp retain the exact primary Dirichlet coefficient and the original radial normalization.

  1. lemma OAI.CubicFirstMoment.cubicThetaInvertedTorus_coefficient line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaInverted_horizontal_coefficient line 28
  3. def OAI.CubicFirstMoment.cubicThetaInvertedFourierObservable line 42
  4. lemma OAI.CubicFirstMoment.cubicThetaInvertedFourier_integrable line 45
  5. lemma OAI.CubicFirstMoment.cubicThetaInvertedFourierObservable_right line 60
  6. lemma OAI.CubicFirstMoment.cubicThetaInvertedFourierObservable_iterated line 76
  7. theorem OAI.CubicFirstMoment.cubicThetaInvertedFourierObservable_normalized line 102