OAI/NumberTheory/PrimePackets/PeriodicTheta.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.ThetaConstruction.periodicPrimalWeight line 138
  2. def OAI.PrimeDegreePackets.ThetaConstruction.periodicDualWeight line 141
  3. def OAI.PrimeDegreePackets.ThetaConstruction.normalizedPeriodicTheta line 144
  4. def OAI.PrimeDegreePackets.ThetaConstruction.periodicPrimalTail line 148
  5. def OAI.PrimeDegreePackets.ThetaConstruction.periodicDualTail line 152
  6. lemma OAI.PrimeDegreePackets.ThetaConstruction.periodicPrimalTail_convergent line 156
  7. lemma OAI.PrimeDegreePackets.ThetaConstruction.periodicDualTail_convergent line 164
  8. lemma OAI.PrimeDegreePackets.ThetaConstruction.periodicPrimalTail_entire line 171
  9. lemma OAI.PrimeDegreePackets.ThetaConstruction.periodicDualTail_entire line 179
  10. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedPeriodicTheta_primal line 186
  11. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedPeriodicTheta_dual line 196
  12. lemma OAI.PrimeDegreePackets.ThetaConstruction.normalizedPeriodicTheta_decomposition line 214
  13. def OAI.PrimeDegreePackets.ThetaConstruction.periodicThetaMellinEntire line 234
  14. lemma OAI.PrimeDegreePackets.ThetaConstruction.periodicThetaMellinEntire_entire line 240
  15. theorem OAI.PrimeDegreePackets.ThetaConstruction.normalizedPeriodicTheta_hasMellin line 250
  16. theorem OAI.PrimeDegreePackets.ThetaConstruction.normalizedPeriodicTheta_mellin_entire line 297
  17. def OAI.PrimeDegreePackets.ThetaConstruction.rationalModulusIdeal line 316
  18. lemma OAI.PrimeDegreePackets.ThetaConstruction.rationalModulusIdeal_restrictScalars line 319
  19. def OAI.PrimeDegreePackets.ThetaConstruction.rationalModulusEquivModN line 329
  20. def OAI.PrimeDegreePackets.ThetaConstruction.integralResidueEquiv line 333
  21. lemma OAI.PrimeDegreePackets.ThetaConstruction.integralResidueEquiv_zero line 338
  22. lemma OAI.PrimeDegreePackets.ThetaConstruction.mulChar_nontrivial_domain line 348
  23. def OAI.PrimeDegreePackets.ThetaConstruction.integralCharacterWeight line 364
  24. lemma OAI.PrimeDegreePackets.ThetaConstruction.integralCharacterWeight_sum_zero line 368
  25. lemma OAI.PrimeDegreePackets.ThetaConstruction.integerCongruenceEquiv_zero line 378
  26. lemma OAI.PrimeDegreePackets.ThetaConstruction.integralCharacterWeight_zero line 383
  27. theorem OAI.PrimeDegreePackets.ThetaConstruction.integralCharacterTheta_hasMellin line 392
  28. theorem OAI.PrimeDegreePackets.ThetaConstruction.integralCharacterTheta_mellin_entire line 404
  29. lemma OAI.PrimeDegreePackets.ThetaConstruction.modN_basis_coordinates line 420
  30. lemma OAI.PrimeDegreePackets.ThetaConstruction.finEquiv_divMod line 427
  31. lemma OAI.PrimeDegreePackets.ThetaConstruction.integralResidueEquiv_coordinates line 438
  32. lemma OAI.PrimeDegreePackets.ThetaConstruction.integralCharacterWeight_coordinates line 456
  33. def OAI.PrimeDegreePackets.ThetaConstruction.modulusScaledBasis line 471
  34. lemma OAI.PrimeDegreePackets.ThetaConstruction.modulusScaledBasis_cancel line 476
  35. def OAI.PrimeDegreePackets.ThetaConstruction.integralOrderTheta line 484
  36. lemma OAI.PrimeDegreePackets.ThetaConstruction.integralOrderTheta_eq_periodic line 490
  37. lemma OAI.PrimeDegreePackets.ThetaConstruction.integralOrderTheta_summable line 504
  38. theorem OAI.PrimeDegreePackets.ThetaConstruction.integralOrderTheta_mellin_entire line 518
  39. lemma OAI.PrimeDegreePackets.ThetaConstruction.integralOrderTheta_mellin_convergent line 530