OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimitiveKernelBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A uniform bound for the normalized primitive kernel at its pole. The only inputs are the proved lattice Gaussian estimates.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimitiveKernel_nonneg line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaPrimitiveKernel_gamma_bound line 20
  3. theorem OAI.CubicFirstMoment.cubicThetaPrimitiveKernel_uniform line 63