OAI/NumberTheory/PrimePackets/CongruenceLattices.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.ThetaConstruction.integerCongruenceEquiv line 139
2. def OAI.PrimeDegreePackets.ThetaConstruction.congruencePoint line 153
3. lemma OAI.PrimeDegreePackets.ThetaConstruction.scaledInteger_congruence line 157
4. lemma OAI.PrimeDegreePackets.ThetaConstruction.scaledInteger_congruence_pair line 170
5. def OAI.PrimeDegreePackets.ThetaConstruction.periodicLatticeTheta line 178
6. lemma OAI.PrimeDegreePackets.ThetaConstruction.congruenceProduct_summable line 183
7. lemma OAI.PrimeDegreePackets.ThetaConstruction.periodicLatticeTheta_summable line 195
8. theorem OAI.PrimeDegreePackets.ThetaConstruction.periodicLatticeTheta_eq_congruenceTheta line 205
9. theorem OAI.PrimeDegreePackets.ThetaConstruction.periodicLatticeTheta_poisson line 218
10. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaRemainder_eq_ofReal line 235
11. lemma OAI.PrimeDegreePackets.ThetaConstruction.thetaRemainder_sum_norm line 243
12. def OAI.PrimeDegreePackets.ThetaConstruction.weightedThetaRemainder line 254
13. lemma OAI.PrimeDegreePackets.ThetaConstruction.weightedThetaRemainder_summable line 260
14. lemma OAI.PrimeDegreePackets.ThetaConstruction.weightedThetaRemainder_bound line 270
15. lemma OAI.PrimeDegreePackets.ThetaConstruction.weightedThetaRemainder_continuousOn line 288
16. lemma OAI.PrimeDegreePackets.ThetaConstruction.weightedThetaRemainder_uniform_exponential_bound line 309
17. def OAI.PrimeDegreePackets.ThetaConstruction.weightedThetaTail line 325
18. lemma OAI.PrimeDegreePackets.ThetaConstruction.weightedThetaTail_locallyIntegrable line 329
19. lemma OAI.PrimeDegreePackets.ThetaConstruction.weightedThetaTail_bigO_exp line 338
20. theorem OAI.PrimeDegreePackets.ThetaConstruction.weightedThetaTail_mellin_differentiable line 351
21. lemma OAI.PrimeDegreePackets.ThetaConstruction.congruenceThetaFourierWeight_bound line 366
22. theorem OAI.PrimeDegreePackets.ThetaConstruction.congruenceDualTail_entire line 375
23. lemma OAI.PrimeDegreePackets.ThetaConstruction.weightedLatticeGaussian_summable line 390
24. lemma OAI.PrimeDegreePackets.ThetaConstruction.weightedLatticeGaussian_decomposition line 400
25. theorem OAI.PrimeDegreePackets.ThetaConstruction.congruenceTheta_poisson_zero_mode line 424
26. theorem OAI.PrimeDegreePackets.ThetaConstruction.congruenceTheta_poisson_of_sum_zero line 443
27. lemma OAI.PrimeDegreePackets.ThetaConstruction.congruenceWeight_bound line 453
28. lemma OAI.PrimeDegreePackets.ThetaConstruction.scaledInteger_gaussian_exponent line 457
29. theorem OAI.PrimeDegreePackets.ThetaConstruction.periodicLatticeTheta_zero_mode line 469
30. def OAI.PrimeDegreePackets.ThetaConstruction.scaledWeightedThetaTail line 489
31. lemma OAI.PrimeDegreePackets.ThetaConstruction.scaledWeightedThetaTail_locallyIntegrable line 493
32. lemma OAI.PrimeDegreePackets.ThetaConstruction.scaledWeightedThetaTail_bigO_exp line 503
33. lemma OAI.PrimeDegreePackets.ThetaConstruction.scaledWeightedThetaTail_bigO_zero line 518
34. lemma OAI.PrimeDegreePackets.ThetaConstruction.scaledWeightedThetaTail_mellin_convergent line 528
35. theorem OAI.PrimeDegreePackets.ThetaConstruction.scaledWeightedThetaTail_mellin_entire line 538