OAI/NumberTheory/DirichletL/Eisenstein/ResidualFourierBounds.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.cuspHeightFourierTest_memLp line 86
  2. def OAI.CubicEisenstein.cuspHeightFourierTestL2 line 94
  3. def OAI.CubicEisenstein.kernelCuspHeightFourier line 98
  4. lemma OAI.CubicEisenstein.kernelCuspHeightFourier_integral line 102
  5. lemma OAI.CubicEisenstein.kernelCuspHeightFourier_restrict line 114
  6. def OAI.CubicEisenstein.kernelCuspHeightFourierFamily line 126
  7. lemma OAI.CubicEisenstein.kernelCuspHeightFourierFamily_analyticAt_nonreal line 132
  8. lemma OAI.CubicEisenstein.kernelCuspHeightFourierFamily_residue_limit line 140
  9. lemma OAI.CubicEisenstein.kernelCuspHeightFourierFamily_initial line 149
  10. def OAI.CubicEisenstein.cuspIntervalWhittakerHeightFactor line 163
  11. lemma OAI.CubicEisenstein.hyperbolicEisenstein_cusp_height_fourier_nonzero line 167
  12. lemma OAI.CubicEisenstein.kernelCuspHeightFourierFamily_initial_factor line 208
  13. lemma OAI.CubicEisenstein.cuspIntervalWhittakerHeightFactor_analyticAt line 215
  14. lemma OAI.CubicEisenstein.kernelCuspHeightFourierFamily_cross_identity line 238
  15. lemma OAI.CubicEisenstein.kernelCuspHeightFourier_residue_factor line 272
  16. lemma OAI.CubicEisenstein.cuspIntervalWhittakerHeightFactor_center_bessel line 312
  17. lemma OAI.CubicEisenstein.kernelCuspHeightFourier_residue_bessel line 325
  18. lemma OAI.CubicEisenstein.kernelCuspHeightFourier_uniform_bound line 344
  19. lemma OAI.CubicEisenstein.cubicResidualFourierCoefficient_interval_bound line 366
  20. def OAI.CubicEisenstein.cubicBesselDensity line 391
  21. lemma OAI.CubicEisenstein.cubicBesselDensity_integrable line 394
  22. lemma OAI.CubicEisenstein.cubicBesselDensity_nonneg line 405
  23. lemma OAI.CubicEisenstein.schlafliIntegral_cubic_real line 408
  24. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_real line 421
  25. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_norm_re line 432
  26. lemma OAI.CubicEisenstein.cubicBesselDensity_upper line 441
  27. lemma OAI.CubicEisenstein.cubicBesselIntegral_upper line 455
  28. def OAI.CubicEisenstein.cubicBesselUpperConstant line 473
  29. lemma OAI.CubicEisenstein.cubicBesselUpperConstant_pos line 476
  30. theorem OAI.CubicEisenstein.schlafliBesselK_cubic_upper line 480
  31. lemma OAI.CubicEisenstein.cubicBesselDensity_lower line 495
  32. lemma OAI.CubicEisenstein.cubicBesselIntegral_lower line 506
  33. def OAI.CubicEisenstein.cubicBesselLowerConstant line 526
  34. lemma OAI.CubicEisenstein.cubicBesselLowerConstant_pos line 529
  35. theorem OAI.CubicEisenstein.schlafliBesselK_cubic_lower line 533
  36. lemma OAI.CubicEisenstein.exp_neg_mul_le_inverse_cube line 565
  37. lemma OAI.CubicEisenstein.summable_exp_neg_embedding_norm line 578
  38. lemma OAI.CubicEisenstein.summable_exp_neg_cuspFrequency_norm line 592
  39. lemma OAI.CubicEisenstein.cubicBesselNormalizer_ne_zero line 612
  40. lemma OAI.CubicEisenstein.cubicBesselHeight_integrable line 622
  41. lemma OAI.CubicEisenstein.cubicBesselHeight_average_lower line 638
  42. lemma OAI.CubicEisenstein.cubicResidualFourierCoefficient_subexponential line 680