OAI/NumberTheory/DirichletL/Eisenstein/WhittakerContinuation.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.cuspWhittakerHeightFactor_analyticAt line 85
  2. lemma OAI.CubicEisenstein.kernelCuspFourierFamily_analyticAt_nonreal line 92
  3. def OAI.CubicEisenstein.continuedNonzeroScattering line 100
  4. def OAI.CubicEisenstein.nonzeroScatteringResidue line 104
  5. lemma OAI.CubicEisenstein.continuedNonzeroScattering_meromorphicAt_center line 108
  6. lemma OAI.CubicEisenstein.continuedNonzeroScattering_meromorphicOn_upper line 113
  7. lemma OAI.CubicEisenstein.continuedNonzeroScattering_residue_limit line 120
  8. lemma OAI.CubicEisenstein.continuedNonzeroScattering_initial line 137
  9. lemma OAI.CubicEisenstein.cuspWhittakerHeightFactor_ne_zero_near_five line 146
  10. lemma OAI.CubicEisenstein.kernelCuspFourierFamily_eq_upper line 158
  11. lemma OAI.CubicEisenstein.continuedNonzeroScattering_eq_upper line 188
  12. lemma OAI.CubicEisenstein.continuedNonzeroScattering_initial_open line 195
  13. lemma OAI.CubicEisenstein.weightedWhittakerIntegrand_integrable line 218
  14. lemma OAI.CubicEisenstein.weightedWhittakerProduct_differentiableAt line 227
  15. lemma OAI.CubicEisenstein.weightedWhittakerProduct_eq_average line 255
  16. theorem OAI.CubicEisenstein.cuspWeightedWhittakerAverage_differentiableAt line 272
  17. theorem OAI.CubicEisenstein.kernelCompact_projection_measure_bound line 285
  18. def OAI.CubicEisenstein.dominatedComplexL2 line 323
  19. lemma OAI.CubicEisenstein.dominatedComplexL2_ae line 336
  20. lemma OAI.CubicEisenstein.dominatedComplexL2_norm_le line 340
  21. def OAI.CubicEisenstein.kernelCompactMultiplicity line 350
  22. lemma OAI.CubicEisenstein.kernelCompactMultiplicity_spec line 353
  23. def OAI.CubicEisenstein.kernelCompactPullbackCLM line 358
  24. theorem OAI.CubicEisenstein.kernelCompactPullbackCLM_ae line 365
  25. lemma OAI.CubicEisenstein.whittaker_bound_integrable_finite line 377
  26. lemma OAI.CubicEisenstein.scaledWhittakerIntegrand_integrable line 388
  27. lemma OAI.CubicEisenstein.scaledWhittakerProduct_differentiableAt line 400
  28. lemma OAI.CubicEisenstein.whittakerIntegrand_scale line 432
  29. lemma OAI.CubicEisenstein.scaledWhittakerProduct_eq_average line 448
  30. theorem OAI.CubicEisenstein.cuspWeightedWhittakerInterval_differentiableAt line 475
  31. def OAI.CubicEisenstein.cuspWeightedFourierPhase line 494
  32. lemma OAI.CubicEisenstein.cuspWeightedFourierPhase_continuous line 497
  33. lemma OAI.CubicEisenstein.cuspWeightedFourierPhase_bound line 501
  34. lemma OAI.CubicEisenstein.cuspWeightedFourierTest_memLp line 506
  35. def OAI.CubicEisenstein.cuspWeightedFourierTestL2 line 512
  36. def OAI.CubicEisenstein.kernelCuspWeightedFourier line 515
  37. lemma OAI.CubicEisenstein.kernelCuspWeightedFourier_integral line 518
  38. lemma OAI.CubicEisenstein.kernelCuspWeightedFourier_restrict line 528
  39. def OAI.CubicEisenstein.kernelCuspWeightedFourierFamily line 541
  40. lemma OAI.CubicEisenstein.kernelCuspWeightedFourierFamily_meromorphicAt line 546
  41. lemma OAI.CubicEisenstein.kernelCuspWeightedFourierFamily_analyticAt_nonreal line 552
  42. lemma OAI.CubicEisenstein.kernelCuspWeightedFourierFamily_residue_limit line 560
  43. lemma OAI.CubicEisenstein.kernelCuspWeightedFourierFamily_initial line 568
  44. def OAI.CubicEisenstein.cuspWeightedWhittakerHeightFactor line 583
  45. lemma OAI.CubicEisenstein.hyperbolicEisenstein_cusp_weighted_fourier_nonzero line 586
  46. lemma OAI.CubicEisenstein.kernelCuspWeightedFourierFamily_initial_factor line 626