OAI/NumberTheory/CubicMoment/Theta/CubicThetaGramRowKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact off-diagonal Gram integrand. Its two additive phases are separated from the common inversion kernel, with the Kubota phase retained.

  1. def OAI.CubicFirstMoment.cubicThetaGramRowPhase line 11
  2. def OAI.CubicFirstMoment.cubicThetaGramInversionKernel line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaFourierProfileTerm_inversion line 20
  4. theorem OAI.CubicFirstMoment.cubicThetaGramRowKernel_identity line 38