OAI/NumberTheory/DirichletL/Eisenstein/EntireMellinProfile.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.finite_mellin_entire line 84
  2. lemma OAI.CubicEisenstein.thetaTwistedCuspProfile_mellin_entire line 106
  3. theorem OAI.CubicEisenstein.completedBesselProfile_mellin_entire_of_periodic line 117
  4. theorem OAI.CubicEisenstein.completedBesselProfile_mellin_entire line 147
  5. lemma OAI.CompletedGauss.mellin_eq_of_positive_eq line 170
  6. lemma OAI.CompletedGauss.continuedBesselDirichlet_finite_sum line 178
  7. lemma OAI.CompletedGauss.besselSmoothingIntegrand_finite_sum line 198
  8. theorem OAI.CompletedGauss.besselSmoothingIntegrand_finite_integrable line 216
  9. def OAI.CubicEisenstein.unramifiedResidualCoefficient line 239
  10. lemma OAI.CubicEisenstein.primeCubicGauss_two_norm line 241
  11. lemma OAI.CubicEisenstein.unramifiedResidualCoefficient_prime_factor line 251
  12. lemma OAI.CubicEisenstein.unramifiedResidualCoefficient_prime_norm line 262
  13. theorem OAI.CubicEisenstein.unramifiedGaussResidue_primary_cube line 270
  14. lemma OAI.CubicEisenstein.unramifiedResidualCoefficient_primary_cube line 285
  15. theorem OAI.CubicEisenstein.unramifiedResidualCoefficient_prime_product_norm line 293
  16. theorem OAI.CubicEisenstein.unramifiedResidualCoefficient_squarefree_cube_norm line 319
  17. def OAI.CubicEisenstein.threeRamifiedUnit line 346
  18. def OAI.CubicEisenstein.traceRamifiedUnit line 347
  19. lemma OAI.CubicEisenstein.three_eq_ramifiedUnit line 349
  20. lemma OAI.CubicEisenstein.trace_eq_ramifiedUnit line 359
  21. def OAI.CubicEisenstein.ramifiedSixUnit line 365
  22. def OAI.CubicEisenstein.ramifiedSixPower line 372
  23. lemma OAI.CubicEisenstein.ramifiedSixPower_bounds line 378
  24. lemma OAI.CubicEisenstein.unitCuspUnramifiedIndex_multiplier line 385
  25. theorem OAI.CubicEisenstein.ramifiedSixIndex_multiplier line 393
  26. theorem OAI.CubicEisenstein.ramifiedBesselValue_prime_power_vanish line 427
  27. lemma OAI.CubicEisenstein.ramified_norm_third line 454
  28. lemma OAI.CubicEisenstein.cubicBesselNormalizer_ramified_mul_norm line 469
  29. def OAI.CubicEisenstein.unramifiedCoefficientBaseBound line 481
  30. lemma OAI.CubicEisenstein.unramifiedCoefficientBaseBound_nonneg line 484
  31. lemma OAI.CubicEisenstein.unramifiedResidualCoefficient_ramified_bound line 487
  32. theorem OAI.CubicEisenstein.unramifiedResidualCoefficient_squarefree_cube_bound line 498
  33. lemma OAI.CubicEisenstein.ramifiedSixWeight_norm_le_one line 517
  34. lemma OAI.CubicEisenstein.ramifiedSixIndex_squarefree_cube line 537
  35. lemma OAI.CubicEisenstein.ramifiedSix_normalized_term_bound line 545
  36. theorem OAI.CubicEisenstein.ramifiedBesselValue_squarefree_cube_bound line 594