OAI/NumberTheory/PrimePackets/GaussianMellin.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.ThetaConstruction.hasMellin_of_add_inversion line 141
  2. def OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedPeriodicTheta line 172
  3. theorem OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedPeriodicTheta_mellin_entire line 177
  4. def OAI.PrimeDegreePackets.complexFlowGaussian line 239
  5. lemma OAI.PrimeDegreePackets.complexFlowGaussian_unit_translate line 244
  6. def OAI.PrimeDegreePackets.residueCharacterFlowTheta line 257
  7. lemma OAI.PrimeDegreePackets.residueCharacterFlowTheta_eq line 263
  8. lemma OAI.PrimeDegreePackets.residueCharacterFlowTheta_unit_covariance line 281
  9. lemma OAI.PrimeDegreePackets.residueCharacterFlowTheta_congruence_periodic line 294
  10. lemma OAI.PrimeDegreePackets.residueCharacterFlowTheta_eq_zero_of_odd line 307
  11. theorem OAI.PrimeDegreePackets.residueCharacterFlowTheta_mellin_entire line 323
  12. lemma OAI.PrimeDegreePackets.periodicLogTheta_boundedAverage_entire line 337
  13. lemma OAI.PrimeDegreePackets.modulusScaledBasis_logScaledLattice line 395
  14. theorem OAI.PrimeDegreePackets.residueCharacterFlowTheta_boundedAverage_entire line 403
  15. lemma OAI.PrimeDegreePackets.ThetaConstruction.moduleResidueEquiv_coordinates line 434
  16. lemma OAI.PrimeDegreePackets.ThetaConstruction.idealCharacterWeight_coordinates line 446
  17. def OAI.PrimeDegreePackets.ThetaConstruction.idealCharacterTheta line 454
  18. lemma OAI.PrimeDegreePackets.ThetaConstruction.idealCharacterTheta_eq_periodic line 460
  19. lemma OAI.PrimeDegreePackets.ThetaConstruction.idealCharacterTheta_mellin_entire line 473
  20. theorem OAI.PrimeDegreePackets.idealCharacterTheta_boundedAverage_entire line 493
  21. def OAI.PrimeDegreePackets.integralIdealFractionalUnit line 525
  22. def OAI.PrimeDegreePackets.integralIdealFullEquiv line 529
  23. lemma OAI.PrimeDegreePackets.integralIdealFullEquiv_coe line 547
  24. def OAI.PrimeDegreePackets.orderedIdealBasis line 550
  25. lemma OAI.PrimeDegreePackets.orderedIdealBasis_coordinates line 555
  26. def OAI.PrimeDegreePackets.idealResidueFlowTheta line 568
  27. lemma OAI.PrimeDegreePackets.idealResidueFlowTheta_eq line 576
  28. theorem OAI.PrimeDegreePackets.idealResidueFlowTheta_boundedAverage_entire line 597