OAI/NumberTheory/DirichletL/Poisson/EisensteinLattice.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EisensteinSchwartzPoisson.inverseJacobian line 61
  2. theorem OAI.EisensteinSchwartzPoisson.integral_comp_linearEquiv line 64
  3. def OAI.EisensteinSchwartzPoisson.dualMap line 76
  4. theorem OAI.EisensteinSchwartzPoisson.inner_linear_dual line 79
  5. theorem OAI.EisensteinSchwartzPoisson.fourier_comp_linearEquiv line 84
  6. def OAI.EisensteinSchwartzPoisson.translateSchwartz line 96
  7. theorem OAI.EisensteinSchwartzPoisson.translateSchwartz_apply line 100
  8. theorem OAI.EisensteinSchwartzPoisson.fourier_translate line 103
  9. def OAI.EisensteinSchwartzPoisson.affinePullback line 110
  10. theorem OAI.EisensteinSchwartzPoisson.affinePullback_apply line 113
  11. theorem OAI.EisensteinSchwartzPoisson.fourier_affinePullback line 116
  12. theorem OAI.EisensteinSchwartzPoisson.affine_lattice_poisson line 125
  13. def OAI.EisensteinSchwartzPoisson.basisMap line 140
  14. theorem OAI.EisensteinSchwartzPoisson.basisMap_apply line 144
  15. def OAI.EisensteinSchwartzPoisson.basisEquiv line 147
  16. theorem OAI.EisensteinSchwartzPoisson.basisEquiv_apply line 177
  17. theorem OAI.EisensteinSchwartzPoisson.basisEquiv_symm_apply line 180
  18. theorem OAI.EisensteinSchwartzPoisson.basisEquiv_det line 184
  19. def OAI.EisensteinSchwartzPoisson.complexMulEquiv line 190
  20. theorem OAI.EisensteinSchwartzPoisson.complexMulEquiv_apply line 193
  21. theorem OAI.EisensteinSchwartzPoisson.complexMulEquiv_symm_apply line 196
  22. theorem OAI.EisensteinSchwartzPoisson.complexMulEquiv_det line 199
  23. def OAI.EisensteinSchwartzPoisson.scaledBasisEquiv line 205
  24. theorem OAI.EisensteinSchwartzPoisson.scaledBasisEquiv_apply line 208
  25. theorem OAI.EisensteinSchwartzPoisson.scaledBasisEquiv_det line 212
  26. abbrev OAI.EisensteinSchwartzPoisson.O line 224
  27. def OAI.EisensteinSchwartzPoisson.eisensteinLatticeMap line 226
  28. theorem OAI.EisensteinSchwartzPoisson.eisensteinLatticeMap_point line 229
  29. theorem OAI.EisensteinSchwartzPoisson.eisenstein_inverseJacobian line 234
  30. def OAI.EisensteinSchwartzPoisson.eisensteinDualFrequency line 243
  31. theorem OAI.EisensteinSchwartzPoisson.actual_eisenstein_coset_poisson line 246
  32. theorem OAI.EisensteinSchwartzPoisson.actual_eisenstein_coset_summable_norm line 271
  33. theorem OAI.EisensteinSchwartzPoisson.actual_eisenstein_summable_norm line 289
  34. theorem OAI.EisensteinSchwartzPoisson.actual_eisenstein_periodic_summable line 293
  35. theorem OAI.EisensteinSchwartzPoisson.actual_eisenstein_periodic_poisson line 307
  36. theorem OAI.EisensteinSchwartzPoisson.inverseJacobian_pos line 333
  37. theorem OAI.EisensteinSchwartzPoisson.dual_lattice_summable_norm line 336
  38. theorem OAI.EisensteinSchwartzPoisson.finite_phase_sum line 350
  39. theorem OAI.EisensteinSchwartzPoisson.actual_eisenstein_periodic_fourier line 374
  40. theorem OAI.EisensteinSchwartzPoisson.dualMap_trans line 400
  41. theorem OAI.EisensteinSchwartzPoisson.dual_basis_apply line 407
  42. theorem OAI.EisensteinSchwartzPoisson.dual_mul_apply line 419
  43. theorem OAI.EisensteinSchwartzPoisson.eisensteinDualFrequency_explicit line 429
  44. def OAI.EisensteinSchwartzPoisson.explicitDualFrequency line 448
  45. theorem OAI.EisensteinSchwartzPoisson.actual_eisenstein_poisson_explicit line 452
  46. def OAI.EisensteinSchwartzPoisson.radialTest line 469
  47. theorem OAI.EisensteinSchwartzPoisson.radialTest_apply line 475
  48. def OAI.EisensteinSchwartzPoisson.compactRadialTest line 478
  49. theorem OAI.EisensteinSchwartzPoisson.compactRadialTest_apply line 482
  50. theorem OAI.EisensteinSchwartzPoisson.actual_radial_poisson line 486
  51. def OAI.IdealGaussCRT.coordinateAddChar line 507
  52. theorem OAI.IdealGaussCRT.addChar_finite_sum line 518
  53. theorem OAI.IdealGaussCRT.addChar_finite_crt_factor line 526
  54. theorem OAI.IdealGaussCRT.gauss_transform_finite_crt line 538
  55. theorem OAI.IdealGaussCRT.gauss_transform_finite_crt_scalar line 563
  56. theorem OAI.IdealGaussCRT.finite_prod_eq_iInf line 587
  57. def OAI.IdealGaussCRT.quotientProdEquivPi line 595
  58. theorem OAI.IdealGaussCRT.quotientProdEquivPi_mk line 601
  59. theorem OAI.IdealGaussCRT.gauss_transform_finite_ideal_crt line 609