OAI/NumberTheory/DirichletL/GaussSum/BesselReflection.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompletedGauss.completedBesselProfile line 84
  2. def OAI.CompletedGauss.besselMellinFactor line 87
  3. def OAI.CompletedGauss.inverseBesselMellinFactor line 91
  4. theorem OAI.CompletedGauss.completedBesselProfile_mellin line 95
  5. lemma OAI.CompletedGauss.inverseBesselMellinFactor_mul line 109
  6. theorem OAI.CompletedGauss.completedDirichletSeries_eq_mellin line 127
  7. theorem OAI.CompletedGauss.inverseBesselMellinFactor_differentiable line 136
  8. theorem OAI.CompletedGauss.inverseBesselMellinFactor_strip_bound line 152
  9. def OAI.CompletedGauss.continuedBesselDirichlet line 183
  10. theorem OAI.CompletedGauss.continuedBesselDirichlet_differentiable line 186
  11. theorem OAI.CompletedGauss.continuedBesselDirichlet_strip_bound line 191
  12. theorem OAI.CompletedGauss.continuedBesselDirichlet_eq_initial line 208
  13. lemma OAI.CubicEisenstein.ramifiedSource_horizontal_hasDerivAt line 223
  14. lemma OAI.CubicEisenstein.ramifiedSource_wirtingerBar_cusp_decay line 241
  15. lemma OAI.CubicEisenstein.ramifiedSource_wirtingerZ_cusp_decay line 273
  16. lemma OAI.CubicEisenstein.ramifiedConjugate_barProfile_isBigO line 305
  17. lemma OAI.CubicEisenstein.ramifiedConjugate_zProfile_isBigO line 319
  18. lemma OAI.CubicEisenstein.reflectedCuspProfile_eq_inv_square line 337
  19. lemma OAI.CubicEisenstein.reflectedCuspProfile_reverse line 343
  20. theorem OAI.CubicEisenstein.cusp_mellin_entire_both line 355
  21. theorem OAI.CubicEisenstein.conjugateSource_ramified_cusp_mellin_entire line 369
  22. theorem OAI.CompletedGauss.squarefree_cube_decomposition_unique line 416
  23. theorem OAI.CompletedGauss.primary_squarefree_cube_eq_iff line 443
  24. theorem OAI.CompletedGauss.primary_squarefree_cube_injective line 469
  25. def OAI.CompletedGauss.besselSmoothingIntegrand line 484
  26. lemma OAI.CompletedGauss.besselSmoothingIntegrand_differentiable line 487
  27. lemma OAI.CompletedGauss.besselSmoothingIntegrand_strip_bound line 498
  28. theorem OAI.CompletedGauss.besselSmoothingIntegrand_contour_eq line 528
  29. theorem OAI.CompletedGauss.completedT_mellin_shift line 550
  30. def OAI.CompletedGauss.besselReflectionFactor line 586
  31. lemma OAI.CompletedGauss.besselMellinFactor_reflection line 590
  32. lemma OAI.CompletedGauss.besselReflectionFactor_norm line 615
  33. theorem OAI.CompletedGauss.continuedBesselDirichlet_reflection line 629