OAI/NumberTheory/PrimePackets/ThetaReflection.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.HeckeMellin.idealThetaXiOn line 105
  2. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXiOn_entire line 112
  3. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXiOn_eq_integral line 119
  4. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXiOn_eq line 168
  5. lemma OAI.PrimeDegreePackets.HeckeMellin.traceDualIdeal_mul_inv line 191
  6. lemma OAI.PrimeDegreePackets.HeckeMellin.traceDualIdeal_involutive line 197
  7. lemma OAI.PrimeDegreePackets.HeckeMellin.traceDualIdeal_norm_product line 202
  8. lemma OAI.PrimeDegreePackets.HeckeMellin.neg_logDomain_fundamental line 231
  9. theorem OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_reflection line 245
  10. lemma OAI.PrimeDegreePackets.HeckeMellin.idealClassFiber_norm_tsum_congr line 290
  11. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaMellin_normalized_congr line 302
  12. theorem OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_normalized_congr line 330
  13. lemma OAI.PrimeDegreePackets.HeckeMellin.traceDual_norm_log line 362
  14. lemma OAI.PrimeDegreePackets.HeckeMellin.norm_sqrt_inv_exp line 369
  15. lemma OAI.PrimeDegreePackets.HeckeMellin.traceDual_functional_factor line 378
  16. lemma OAI.PrimeDegreePackets.HeckeMellin.completion_reflection_factor line 391
  17. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_normalized_reflection line 405
  18. def OAI.PrimeDegreePackets.HeckeMellin.traceDualClassEquiv line 420
  19. lemma OAI.PrimeDegreePackets.HeckeMellin.traceDualClassEquiv_apply line 424
  20. lemma OAI.PrimeDegreePackets.HeckeMellin.classThetaXi_reflection line 430
  21. theorem OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_functionalEquation line 459
  22. lemma OAI.PrimeDegreePackets.HeckeMellin.totallyRealCompletedXi_real line 478
  23. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_conj line 490
  24. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_one line 504
  25. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_zero line 517
  26. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_ne_zero_of_re_gt_one line 524
  27. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_ne_zero_of_re_neg line 531
  28. def OAI.PrimeDegreePackets.HeckeMellin.dedekindXiZeros line 542
  29. lemma OAI.PrimeDegreePackets.HeckeMellin.dedekindXiZeros_re_mem_Icc line 546
  30. lemma OAI.PrimeDegreePackets.HeckeMellin.dedekindXiZeros_ne_one line 556
  31. lemma OAI.PrimeDegreePackets.HeckeMellin.dedekindXiZeros_ne_zero line 564