OAI/NumberTheory/PrimePackets/RealMellin.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PrimeDegreePackets.HeckeMellin.classTheta_mellin_lintegral_totallyReal line 131
2. lemma OAI.PrimeDegreePackets.HeckeMellin.nonnegativeIdealThetaMellin_ne_top_totallyReal line 157
3. theorem OAI.PrimeDegreePackets.HeckeMellin.integrable_idealThetaMellinKernel_totallyReal line 168
4. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_eq_integral_totallyReal line 186
5. lemma OAI.PrimeDegreePackets.HeckeMellin.classTheta_mellin_integral_real_totallyReal line 238
6. theorem OAI.PrimeDegreePackets.HeckeMellin.classThetaXi_real_eq_totallyReal line 260
7. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_real_eq_totallyReal line 296
8. theorem OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_eq_totallyReal line 320
9. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_not_identically_zero_totallyReal line 328
10. lemma OAI.PrimeDegreePackets.HeckeMellin.regularizedThetaZeta_eq_totallyReal line 340
11. theorem OAI.PrimeDegreePackets.HeckeMellin.regularizedThetaZeta_one_totallyReal line 355
12. lemma OAI.PrimeDegreePackets.HeckeMellin.regularizedThetaZeta_eventually_ne_zero_totallyReal line 369
13. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_logDeriv_totallyReal line 378
14. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXiOn_eq_integral_totallyReal line 394
15. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXiOn_eq_totallyReal line 441
16. theorem OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_reflection_totallyReal line 464
17. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaMellin_normalized_congr_totallyReal line 509
18. theorem OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_normalized_congr_totallyReal line 535