OAI/NumberTheory/DirichletL/Eisenstein/ReflectedCuspMellin.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.reflectedCuspProfile line 83
  2. lemma OAI.CubicEisenstein.reflectedCuspProfile_mellin line 86
  3. lemma OAI.CubicEisenstein.reflectedCuspProfile_mellinConvergent line 93
  4. lemma OAI.CubicEisenstein.cusp_truncation_reflection_ae line 109
  5. theorem OAI.CubicEisenstein.cusp_mellin_entire line 128
  6. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.directionalTerm line 179
  7. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.term_horizontal_hasDerivAt line 182
  8. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.directionalTerm_slab_bound line 198
  9. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.directionalTerm_summable line 214
  10. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_horizontal_hasDerivAt line 221
  11. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_horizontal_hasDerivAt line 232
  12. theorem OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_wirtingerBar line 241
  13. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_wirtingerBar_summable line 256
  14. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.term_cusp_bound line 272
  15. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.directionalTerm_cusp_majorant line 309
  16. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.directionalSeries_cusp_decay line 344
  17. theorem OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_wirtingerBar_cusp_decay line 369
  18. lemma OAI.CubicEisenstein.spatialComplexSplit_differentiable line 406
  19. lemma OAI.CubicEisenstein.spatialComplexSplit_symm_differentiable line 410
  20. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_euclidean_differentiableAt line 429
  21. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_translate_cusp_differentiableAt line 435
  22. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_translate_split_differentiableAt line 447
  23. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_translate_split_differentiableAt line 457
  24. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_split_differentiableAt line 465
  25. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_wirtingerBar line 470
  26. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_wirtingerBar_cusp_decay line 476
  27. lemma OAI.CubicEisenstein.horizontalPhaseMultiplier_wirtingerZ line 487
  28. lemma OAI.CubicEisenstein.horizontalWirtingerBar_star line 496
  29. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_wirtingerZ line 505
  30. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_wirtingerZ_cusp_decay line 520
  31. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_wirtingerZ line 548
  32. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_wirtingerZ_cusp_decay line 554
  33. def OAI.CubicEisenstein.cubicSourceConjugateFunction line 561
  34. lemma OAI.CubicEisenstein.cubicSourceConjugateFunction_translate_split_differentiableAt line 563
  35. lemma OAI.CubicEisenstein.cubicSourceConjugateFunction_wirtingerBar_cusp_decay line 569
  36. lemma OAI.CubicEisenstein.horizontalWirtingerBar_translate line 584
  37. lemma OAI.CubicEisenstein.cuspDerivative_of_transform line 596
  38. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_levelThree line 638
  39. lemma OAI.CubicEisenstein.cubicSourceConjugateFunction_levelThree line 648
  40. theorem OAI.CubicEisenstein.cubicSourceResidualFunction_cuspDerivative line 654
  41. theorem OAI.CubicEisenstein.cubicSourceConjugateFunction_cuspDerivative line 668