OAI/NumberTheory/CubicGram/LatticePoisson.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Eisenstein real coordinates, measure factors and translated lattice Poisson summation.

  1. def OAI.CubicFirstMoment.complexOfRealCoords line 17
  2. lemma OAI.CubicFirstMoment.complexOfRealCoords_injective line 25
  3. lemma OAI.CubicFirstMoment.complexOfRealCoords_surjective line 45
  4. def OAI.CubicFirstMoment.eisensteinRealCoords line 50
  5. lemma OAI.CubicFirstMoment.eisensteinRealCoords_apply line 54
  6. lemma OAI.CubicFirstMoment.eisensteinRealCoords_integer line 57
  7. def OAI.CubicFirstMoment.realCoordMatrix line 61
  8. lemma OAI.CubicFirstMoment.realCoordMatrix_det line 64
  9. lemma OAI.CubicFirstMoment.realCoordMatrix_apply line 67
  10. lemma OAI.CubicFirstMoment.eisensteinRealCoords_map_volume line 74
  11. lemma OAI.CubicFirstMoment.integral_eisensteinRealCoords line 92
  12. def OAI.CubicFirstMoment.traceLambda line 100
  13. lemma OAI.CubicFirstMoment.traceLambda_eq line 102
  14. lemma OAI.CubicFirstMoment.traceLambda_ne_zero line 107
  15. def OAI.CubicFirstMoment.tracePair line 111
  16. def OAI.CubicFirstMoment.traceFourier line 113
  17. def OAI.CubicFirstMoment.dualRealCoords line 116
  18. lemma OAI.CubicFirstMoment.dualRealCoords_trace line 119
  19. lemma OAI.CubicFirstMoment.dualRealCoords_eq line 130
  20. def OAI.CubicFirstMoment.dualIntegerEquiv line 141
  21. def OAI.CubicFirstMoment.eisensteinPullback line 147
  22. lemma OAI.CubicFirstMoment.coordinateFourier_eisenstein line 150
  23. lemma OAI.CubicFirstMoment.coordinatesEquiv_coe line 161
  24. lemma OAI.CubicFirstMoment.dualRealCoords_integer line 165
  25. theorem OAI.CubicFirstMoment.poisson_eisenstein line 171
  26. lemma OAI.CubicFirstMoment.tracePair_add_left line 197
  27. lemma OAI.CubicFirstMoment.traceFourier_translation line 202
  28. theorem OAI.CubicFirstMoment.poisson_eisenstein_translate line 215
  29. def OAI.CubicFirstMoment.complexMulEquiv line 226
  30. lemma OAI.CubicFirstMoment.complexMulEquiv_apply line 229
  31. def OAI.CubicFirstMoment.complexMulMatrix line 232
  32. lemma OAI.CubicFirstMoment.complexMulMatrix_det line 235
  33. lemma OAI.CubicFirstMoment.complexMulMatrix_apply line 239
  34. lemma OAI.CubicFirstMoment.complexMul_map_volume line 247
  35. lemma OAI.CubicFirstMoment.integral_complexMul line 271
  36. lemma OAI.CubicFirstMoment.traceFourier_complexMul line 281
  37. theorem OAI.CubicFirstMoment.poisson_eisenstein_coset line 294