OAI/NumberTheory/CubicMoment/Theta/CubicThetaFourierRadial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact separated radial operator for the trace-Fourier lattice. This retains the factor four between the heat scale and the Laplacian potential.

  1. lemma OAI.CubicFirstMoment.cubicThetaHyperbolicOperator_fourier line 11
  2. def OAI.CubicFirstMoment.cubicThetaFourierLogLift line 25
  3. theorem OAI.CubicFirstMoment.cubicThetaFourierLogLift_equation line 28
  4. lemma OAI.CubicFirstMoment.cubicThetaFourierRadial_scale line 46
  5. theorem OAI.CubicFirstMoment.cubicThetaFourierLogLift_lattice_equation line 51