OAI/NumberTheory/CubicMoment/Theta/CubicThetaFourierStripUnfold.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Full arithmetic unfolding of the compact Fourier profile. The positive cutoff can lie below the injective cusp, since the group sum is unfolded first.

  1. lemma OAI.CubicFirstMoment.cubicThetaFourierStripSeed_group_sum line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaPositiveFourierProfile_pairing_integral line 49