OAI/NumberTheory/CubicGram/GramPoisson.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The literal character Gram kernel and normalized radial Poisson expansion.

  1. lemma OAI.CubicFirstMoment.hasCompactSupport_normProfile line 21
  2. lemma OAI.CubicFirstMoment.contDiff_normProfile line 32
  3. def OAI.CubicFirstMoment.primaryCharacterGram line 42
  4. def OAI.CubicFirstMoment.gramDyad line 46
  5. def OAI.CubicFirstMoment.CharacterGramStatement line 49
  6. def OAI.CubicFirstMoment.primaryCosetMap line 58
  7. lemma OAI.CubicFirstMoment.primaryCosetMap_bijective line 67
  8. lemma OAI.CubicFirstMoment.tsum_primary_eq_coset line 81
  9. def OAI.CubicFirstMoment.normProfileSchwartz line 90
  10. lemma OAI.CubicFirstMoment.normProfileSchwartz_apply line 94
  11. def OAI.CubicFirstMoment.normProfileFourier line 98
  12. lemma OAI.CubicFirstMoment.primaryMixedFourier_zero line 101
  13. lemma OAI.CubicFirstMoment.traceFourier_normProfile line 111
  14. theorem OAI.CubicFirstMoment.primaryCharacterGram_poisson line 130
  15. def OAI.CubicFirstMoment.gramDualTerm line 157
  16. lemma OAI.CubicFirstMoment.norm_gramGauss_scalar line 163
  17. lemma OAI.CubicFirstMoment.gramDualTerm_zero line 169
  18. theorem OAI.CubicFirstMoment.primaryCharacterGram_poisson_normalized line 183
  19. theorem OAI.CubicFirstMoment.norm_primaryCharacterGram_poisson line 212
  20. lemma OAI.CubicFirstMoment.normProfileFourier_mul_unit line 227
  21. lemma OAI.CubicFirstMoment.normProfileFourier_eq_of_normSq_eq line 244
  22. def OAI.CubicFirstMoment.radialDualProfile line 254
  23. lemma OAI.CubicFirstMoment.normProfileFourier_radial line 257
  24. lemma OAI.CubicFirstMoment.gramDualTerm_radial line 262