OAI/NumberTheory/PrimePackets/LatticeTheta.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.fullLatticeEuclideanBasis line 89
  2. lemma OAI.PrimeDegreePackets.fullLatticeEuclideanBasis_det line 94
  3. lemma OAI.PrimeDegreePackets.fullLatticeEuclideanBasis_apply line 101
  4. def OAI.PrimeDegreePackets.fullLatticeTheta line 113
  5. lemma OAI.PrimeDegreePackets.fullLatticeTheta_eq line 116
  6. theorem OAI.PrimeDegreePackets.fullLatticeTheta_inversion line 127
  7. lemma OAI.PrimeDegreePackets.sum_orderedEmbeddings line 142
  8. def OAI.PrimeDegreePackets.traceDualFullLattice line 152
  9. lemma OAI.PrimeDegreePackets.traceDualFullLattice_basis line 160
  10. lemma OAI.PrimeDegreePackets.traceDualFullLattice_carrier line 166
  11. lemma OAI.PrimeDegreePackets.traceDual_embeddingMatrix_mul line 173
  12. lemma OAI.PrimeDegreePackets.fullLatticeEuclideanBasis_toLinearMap line 189
  13. lemma OAI.PrimeDegreePackets.traceDualFullLattice_euclideanBasis line 195
  14. theorem OAI.PrimeDegreePackets.fullLatticeTheta_traceDual line 221
  15. def OAI.PrimeDegreePackets.ThetaConstruction.normalizedTheta line 235
  16. def OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail line 238
  17. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedTheta_inversion line 241
  18. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail_locallyIntegrable line 254
  19. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail_bigO_exp line 262
  20. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail_bigO_zero line 271
  21. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail_mellin_convergent line 279
  22. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail_mellin_differentiable line 286
  23. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedThetaTail_eq line 294
  24. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedTheta_decomposition line 299
  25. def OAI.PrimeDegreePackets.ThetaConstruction.thetaMellinContinuation line 323
  26. def OAI.PrimeDegreePackets.ThetaConstruction.thetaMellinXi line 330
  27. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaMellinXi_differentiable line 336
  28. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaMellinXi_eq line 341
  29. lemma OAI.PrimeDegreePackets.ThetaConstruction.mellinConvergent_inv line 348
  30. theorem OAI.PrimeDegreePackets.ThetaConstruction.normalizedTheta_hasMellin line 354
  31. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaDual_involutive line 408
  32. lemma OAI.PrimeDegreePackets.ThetaConstruction.adjointEquiv_det line 416
  33. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaDual_det line 426
  34. theorem OAI.PrimeDegreePackets.ThetaConstruction.thetaMellinXi_functional_equation line 433
  35. def OAI.PrimeDegreePackets.fullLatticeThetaXi line 460
  36. theorem OAI.PrimeDegreePackets.fullLatticeThetaXi_differentiable line 463
  37. theorem OAI.PrimeDegreePackets.fullLatticeThetaXi_functional_equation line 467
  38. theorem OAI.PrimeDegreePackets.fullLatticeTheta_hasMellin line 476
  39. lemma OAI.PrimeDegreePackets.ThetaConstruction.gaussian_hasMellin line 489
  40. def OAI.PrimeDegreePackets.ThetaConstruction.latticeEnergy line 500
  41. lemma OAI.PrimeDegreePackets.ThetaConstruction.latticeEnergy_pos line 503
  42. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaRemainder_eq_real_sum line 508
  43. lemma OAI.PrimeDegreePackets.ThetaConstruction.realGaussian_summable line 520
  44. def OAI.PrimeDegreePackets.ThetaConstruction.latticeEpsteinSeries line 533
  45. lemma OAI.PrimeDegreePackets.ThetaConstruction.mellinGaussian_norm_sum line 536
  46. theorem OAI.PrimeDegreePackets.ThetaConstruction.thetaMellinContinuation_hasSum_epstein line 553
  47. lemma OAI.PrimeDegreePackets.ThetaConstruction.latticeEpsteinSeries_summable line 602
  48. theorem OAI.PrimeDegreePackets.ThetaConstruction.thetaMellinContinuation_eq_epstein line 610