OAI/NumberTheory/CubicMoment/Theta/CubicThetaThetaObservation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual weighted Fourier observations of the theta residue. The arithmetic value of the nonzero Whittaker coefficient remains to be identified.

  1. def OAI.CubicFirstMoment.cubicThetaObservedWhittakerCoefficient line 14
  2. theorem OAI.CubicFirstMoment.cubicThetaResidue_whittaker_observation line 18
  3. theorem OAI.CubicFirstMoment.cubicThetaResidue_zero_observation line 31