OAI/NumberTheory/PrimePackets/IdealThetaXi.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi line 100
  2. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_entire line 108
  3. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_eq_integral line 115
  4. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaMellinKernel_real line 161
  5. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaMellinIntegral_real line 179
  6. lemma OAI.PrimeDegreePackets.HeckeMellin.classTheta_mellin_integral_real line 209
  7. def OAI.PrimeDegreePackets.HeckeMellin.classThetaXi line 232
  8. lemma OAI.PrimeDegreePackets.HeckeMellin.classThetaXi_entire line 239
  9. lemma OAI.PrimeDegreePackets.HeckeMellin.dedekindZeta_real_value line 249
  10. theorem OAI.PrimeDegreePackets.HeckeMellin.classThetaXi_real_eq line 256
  11. lemma OAI.PrimeDegreePackets.HeckeMellin.hecke_factor_cancellation line 291
  12. lemma OAI.PrimeDegreePackets.HeckeMellin.halfPlane_eq_of_real_eq line 301
  13. lemma OAI.PrimeDegreePackets.HeckeMellin.realHeckeFactor_ofReal line 330
  14. lemma OAI.PrimeDegreePackets.HeckeMellin.conductor_pi_factor line 340
  15. def OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi line 351
  16. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_entire line 357
  17. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_real_eq line 363
  18. theorem OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_eq line 389
  19. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_not_identically_zero line 397
  20. def OAI.PrimeDegreePackets.HeckeMellin.regularizedThetaZeta line 412
  21. lemma OAI.PrimeDegreePackets.HeckeMellin.regularizedThetaZeta_differentiableAt line 419
  22. lemma OAI.PrimeDegreePackets.HeckeMellin.regularizedThetaZeta_eq line 432
  23. theorem OAI.PrimeDegreePackets.HeckeMellin.regularizedThetaZeta_one line 449
  24. lemma OAI.PrimeDegreePackets.HeckeMellin.regularizedThetaZeta_eventually_ne_zero line 463
  25. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_logDeriv line 474
  26. lemma OAI.PrimeDegreePackets.HeckeMellin.entire_eq_of_real_eq line 491
  27. lemma OAI.PrimeDegreePackets.HeckeMellin.arithmeticFlowTheta_eq_sum line 501
  28. lemma OAI.PrimeDegreePackets.HeckeMellin.arithmeticFlowTheta_carrier_congr line 514
  29. lemma OAI.PrimeDegreePackets.HeckeMellin.thetaMellinXi_congr_of_normalizedTheta line 527
  30. lemma OAI.PrimeDegreePackets.HeckeMellin.arithmeticFlowThetaXi_carrier_congr line 551
  31. def OAI.PrimeDegreePackets.HeckeMellin.traceDualIdeal line 563
  32. lemma OAI.PrimeDegreePackets.HeckeMellin.traceDualIdeal_carrier line 567