OAI/NumberTheory/CubicMoment/Theta/CubicThetaFourierProfileSection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual compact automorphic sections attached to nonzero Fourier tests.

  1. theorem OAI.CubicFirstMoment.cubicThetaFourierProfileSeries_core line 11
  2. def OAI.CubicFirstMoment.cubicThetaFourierProfileSection line 36
  3. lemma OAI.CubicFirstMoment.cubicThetaFourierProfileSection_compact line 47
  4. lemma OAI.CubicFirstMoment.cubicThetaFourierProfileTerm_zeroRow line 59
  5. theorem OAI.CubicFirstMoment.cubicThetaFourierProfileSeries_high line 79