OAI/NumberTheory/CubicMoment/Estimates/ResidueHarmonicPoisson.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Periodic Poisson for the actual positive and negative angular polynomial Gaussians. The finite Fourier coefficient is retained exactly.

  1. def OAI.CubicFirstMoment.residueHarmonicTheta line 12
  2. def OAI.CubicFirstMoment.residueAntiHarmonicTheta line 17
  3. lemma OAI.CubicFirstMoment.residueHarmonic_poisson line 22
  4. lemma OAI.CubicFirstMoment.residueAntiHarmonic_poisson line 45