OAI/NumberTheory/PrimePackets/CoordinateLattices.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.ThetaConstruction.integerVector_closedEmbedding line 81
  2. lemma OAI.PrimeDegreePackets.ThetaConstruction.integerVector_tendsto line 84
  3. def OAI.PrimeDegreePackets.ThetaConstruction.coordinateLattice line 87
  4. instance OAI.PrimeDegreePackets.ThetaConstruction.coordinateLattice_discrete line 90
  5. instance OAI.PrimeDegreePackets.ThetaConstruction.coordinateLattice_full line 93
  6. lemma OAI.PrimeDegreePackets.ThetaConstruction.integerVector_mem line 96
  7. def OAI.PrimeDegreePackets.ThetaConstruction.integerVectorInLattice line 101
  8. lemma OAI.PrimeDegreePackets.ThetaConstruction.integerVectorInLattice_injective line 104
  9. lemma OAI.PrimeDegreePackets.ThetaConstruction.coordinateLattice_rank line 110
  10. lemma OAI.PrimeDegreePackets.ThetaConstruction.summable_integerVector_rpow line 114
  11. lemma OAI.PrimeDegreePackets.ThetaConstruction.schwartz_locallyNormal line 122
  12. lemma OAI.PrimeDegreePackets.ThetaConstruction.locallyNormal_of_polynomial_decay line 166
  13. lemma OAI.PrimeDegreePackets.ThetaConstruction.gaussian_polynomial_bound line 200
  14. def OAI.PrimeDegreePackets.ThetaConstruction.coordinateGaussian line 214
  15. lemma OAI.PrimeDegreePackets.ThetaConstruction.coordinateGaussian_decay line 218
  16. lemma OAI.PrimeDegreePackets.ThetaConstruction.coordinateGaussian_locallyNormal line 238
  17. lemma OAI.PrimeDegreePackets.ThetaConstruction.integral_comp_linearEquiv line 250
  18. lemma OAI.PrimeDegreePackets.ThetaConstruction.integrable_comp_linearEquiv_iff line 259
  19. lemma OAI.PrimeDegreePackets.ThetaConstruction.fourier_comp_linearEquiv line 268
  20. lemma OAI.PrimeDegreePackets.ThetaConstruction.schwartzCM_apply line 286
  21. def OAI.PrimeDegreePackets.ThetaConstruction.euclideanSchwartz line 289
  22. def OAI.PrimeDegreePackets.ThetaConstruction.coordinateFourier line 292
  23. lemma OAI.PrimeDegreePackets.ThetaConstruction.fourierCharacter_eq line 296
  24. lemma OAI.PrimeDegreePackets.ThetaConstruction.coordinateFourier_apply line 310
  25. lemma OAI.PrimeDegreePackets.ThetaConstruction.summable_schwartz_integerVector line 329
  26. lemma OAI.PrimeDegreePackets.ThetaConstruction.schwartz_multivariate_poisson line 335
  27. def OAI.PrimeDegreePackets.ThetaConstruction.adjointEquiv line 352
  28. def OAI.PrimeDegreePackets.ThetaConstruction.euclideanInteger line 371
  29. def OAI.PrimeDegreePackets.ThetaConstruction.coordinateBasis line 373
  30. def OAI.PrimeDegreePackets.ThetaConstruction.latticeTheta line 376
  31. lemma OAI.PrimeDegreePackets.ThetaConstruction.summable_of_locallyNormal line 379
  32. lemma OAI.PrimeDegreePackets.ThetaConstruction.latticeTheta_summable line 385
  33. lemma OAI.PrimeDegreePackets.ThetaConstruction.coordinate_fourierIntegral line 391
  34. lemma OAI.PrimeDegreePackets.ThetaConstruction.coordinateGaussian_integrable line 410
  35. lemma OAI.PrimeDegreePackets.ThetaConstruction.coordinateGaussian_fourier line 421
  36. theorem OAI.PrimeDegreePackets.ThetaConstruction.latticeTheta_inversion line 443
  37. abbrev OAI.PrimeDegreePackets.ThetaConstruction.NonzeroIntegerVector line 466
  38. def OAI.PrimeDegreePackets.ThetaConstruction.thetaRemainder line 468
  39. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaRemainder_summable line 471
  40. lemma OAI.PrimeDegreePackets.ThetaConstruction.gaussianTerm_norm line 476
  41. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaRemainder_eq line 480
  42. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaRemainder_continuousOn line 498
  43. lemma OAI.PrimeDegreePackets.ThetaConstruction.euclideanInteger_norm_one_le line 514
  44. lemma OAI.PrimeDegreePackets.ThetaConstruction.theta_lattice_lower_bound line 523
  45. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaRemainder_exponential_bound line 538
  46. def OAI.PrimeDegreePackets.ThetaConstruction.thetaTail line 565
  47. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaTail_locallyIntegrable line 568
  48. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaTail_bigO_exp line 575
  49. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaTail_mellin_differentiable line 583