OAI/NumberTheory/DirichletL/Eisenstein/SourceBesselExpansion.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.opposite_height_fourier_average line 85
  2. lemma OAI.CubicEisenstein.oppositeHeight_cross_identity line 118
  3. theorem OAI.CubicEisenstein.translatedHeightFourier_opposite_residue line 149
  4. lemma OAI.CubicEisenstein.rational_height_fourier_right_T line 184
  5. lemma OAI.CubicEisenstein.translatedHeightFourier_residue_scaled_of_initial line 220
  6. lemma OAI.CubicEisenstein.translatedHeightFourier_one line 262
  7. lemma OAI.CubicEisenstein.translatedHeightFourier_bruhat line 267
  8. theorem OAI.CubicEisenstein.kernelSourceProjection_height_fourier line 293
  9. lemma OAI.CubicEisenstein.cuspIntervalWhittakerHeightFactor_zero_center line 318
  10. lemma OAI.CubicEisenstein.kernelCuspHeightFourier_principal_residue line 330
  11. lemma OAI.CubicEisenstein.principalArithmeticResidue_not_horizontal line 340
  12. theorem OAI.CubicEisenstein.kernelSourceProjection_height_residue line 346
  13. def OAI.CubicEisenstein.sourceResidualFourierCoefficient line 357
  14. def OAI.CubicEisenstein.sourceResidualFullModeAmplitude line 359
  15. lemma OAI.CubicEisenstein.sourceResidualFullModeAmplitude_zero_density line 363
  16. lemma OAI.CubicEisenstein.sourceResidualFullModeAmplitude_nonzero_density line 369
  17. lemma OAI.CubicEisenstein.kernelSourceProjection_height_bessel line 376
  18. theorem OAI.CubicEisenstein.kernelSourceProjection_height_full line 385
  19. lemma OAI.CubicEisenstein.sourceResidualFourierCoefficient_interval_bound line 419
  20. lemma OAI.CubicEisenstein.sourceResidualFourierCoefficient_subexponential line 436
  21. def OAI.CubicEisenstein.sourceBesselCoefficients line 462
  22. def OAI.CubicEisenstein.sourceBesselFunction line 466
  23. lemma OAI.CubicEisenstein.sourceBesselFunction_continuous line 469
  24. lemma OAI.CubicEisenstein.sourceBesselFunction_fourier line 472
  25. lemma OAI.CubicEisenstein.sourceBesselFunction_period line 481
  26. lemma OAI.CubicEisenstein.sourceBesselFunction_height_memLp line 486
  27. lemma OAI.CubicEisenstein.sourceResidualFullMode_density_integrable line 497
  28. lemma OAI.CubicEisenstein.projectedResidue_slice_coefficient_ae line 517
  29. lemma OAI.CubicEisenstein.projectedResidue_all_slice_coefficients_ae line 529
  30. lemma OAI.CubicEisenstein.projectedResidue_all_fourier_integrals_ae line 536
  31. theorem OAI.CubicEisenstein.projectedResidue_cell_slices_ae line 551
  32. theorem OAI.CubicEisenstein.sourceBesselFunction_represents_projection line 566
  33. theorem OAI.CubicEisenstein.cubicSourceResidualFunction_eq_bessel line 577
  34. theorem OAI.CubicEisenstein.cubicSourceResidualFunction_fourier_full line 584
  35. theorem OAI.CubicEisenstein.cubicSourceResidualFunction_bessel line 591
  36. theorem OAI.CubicEisenstein.sourceResidual_series_uniform line 601
  37. theorem OAI.CubicEisenstein.sourceResidual_bessel_normal line 606