OAI/NumberTheory/CubicGauss/ResiduePoisson.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Residue-class theta transforms and primitive additive trace characters.

  1. def OAI.CubicFirstMoment.HeckeTheta.residueCosetMap line 14
  2. lemma OAI.CubicFirstMoment.HeckeTheta.residueCosetMap_bijective line 17
  3. def OAI.CubicFirstMoment.HeckeTheta.residueCosetEquiv line 37
  4. lemma OAI.CubicFirstMoment.HeckeTheta.residueCosetEquiv_apply line 41
  5. lemma OAI.CubicFirstMoment.HeckeTheta.norm_pos line 45
  6. lemma OAI.CubicFirstMoment.HeckeTheta.coe_ne_zero line 48
  7. lemma OAI.CubicFirstMoment.HeckeTheta.coset_norm line 51
  8. lemma OAI.CubicFirstMoment.HeckeTheta.coset_gaussian_poisson line 61
  9. def OAI.CubicFirstMoment.HeckeTheta.residueFourier line 82
  10. def OAI.CubicFirstMoment.HeckeTheta.residueTheta line 87
  11. lemma OAI.CubicFirstMoment.HeckeTheta.weighted_lattice_gaussian_summable line 91
  12. lemma OAI.CubicFirstMoment.HeckeTheta.phase_gaussian_summable line 106
  13. theorem OAI.CubicFirstMoment.HeckeTheta.residue_theta_poisson line 121
  14. lemma OAI.CubicFirstMoment.HeckeTheta.tracePhase_add_right line 150
  15. lemma OAI.CubicFirstMoment.HeckeTheta.tracePhase_integral line 157
  16. lemma OAI.CubicFirstMoment.HeckeTheta.tracePhase_modulus_congr line 167
  17. def OAI.CubicFirstMoment.HeckeTheta.residueTraceChar line 182
  18. lemma OAI.CubicFirstMoment.HeckeTheta.residueTraceChar_mk line 198
  19. lemma OAI.CubicFirstMoment.HeckeTheta.residueTraceChar_mul_mk line 203
  20. lemma OAI.CubicFirstMoment.HeckeTheta.phase_real_eq_one_iff line 211
  21. lemma OAI.CubicFirstMoment.HeckeTheta.trace_dual_integral line 227
  22. theorem OAI.CubicFirstMoment.HeckeTheta.residueTraceChar_primitive line 249