OAI/NumberTheory/CubicGram/MixedPoisson.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Primary mixed characters and squarefree coset Poisson summation.

  1. lemma OAI.CubicFirstMoment.cubicSymbol_cube_of_isCoprime line 19
  2. lemma OAI.CubicFirstMoment.cubicSymbol_three_lambda line 31
  3. def OAI.CubicFirstMoment.mixedSymbol line 38
  4. lemma OAI.CubicFirstMoment.mixedSymbol_mul line 40
  5. lemma OAI.CubicFirstMoment.mixedSymbol_three_lambda line 45
  6. lemma OAI.CubicFirstMoment.mixedSymbol_congr line 50
  7. def OAI.CubicFirstMoment.primaryMixedFourier line 64
  8. lemma OAI.CubicFirstMoment.primaryMixedFourier_eq line 69
  9. theorem OAI.CubicFirstMoment.primaryMixedFourier_squarefree line 111
  10. lemma OAI.CubicFirstMoment.traceFourier_affine line 123
  11. theorem OAI.CubicFirstMoment.poisson_eisenstein_periodic_coset line 130
  12. theorem OAI.CubicFirstMoment.poisson_primary_mixed_squarefree line 159