OAI/NumberTheory/DirichletL/Eisenstein/HyperbolicSpace.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.compactSubgroup line 80
  2. abbrev OAI.CubicEisenstein.HyperbolicSpace line 97
  3. def OAI.CubicEisenstein.hyperbolicEisenstein line 99
  4. lemma OAI.CubicEisenstein.hyperbolicEisenstein_mk line 107
  5. theorem OAI.CubicEisenstein.hyperbolicEisenstein_automorphy line 110
  6. def OAI.CubicEisenstein.upperPoint line 117
  7. lemma OAI.CubicEisenstein.hyperbolicEisenstein_upperPoint line 120
  8. def OAI.CubicEisenstein.complexBottomRow line 123
  9. lemma OAI.CubicEisenstein.complexBottomRow_mul line 125
  10. lemma OAI.CubicEisenstein.complexBottomRow_ne_zero line 131
  11. def OAI.CubicEisenstein.liftedHeight line 140
  12. lemma OAI.CubicEisenstein.liftedHeight_pos line 142
  13. lemma OAI.CubicEisenstein.liftedHeight_right_unitary line 145
  14. def OAI.CubicEisenstein.hyperbolicHeight line 149
  15. lemma OAI.CubicEisenstein.hyperbolicHeight_mk line 157
  16. lemma OAI.CubicEisenstein.hyperbolicHeight_pos line 160
  17. theorem OAI.CubicEisenstein.hyperbolicHeight_action_upperPoint line 163
  18. def OAI.CubicEisenstein.cosetHeight line 170
  19. lemma OAI.CubicEisenstein.cosetHeight_cosetOf line 177
  20. theorem OAI.CubicEisenstein.hyperbolicEisenstein_eq_height_series line 185
  21. theorem OAI.CubicEisenstein.height_series_summable_norm line 197
  22. theorem OAI.CubicEisenstein.hyperbolicEisenstein_differentiableOn line 210
  23. def OAI.CubicEisenstein.upperTranslation line 219
  24. lemma OAI.CubicEisenstein.complexCharacter_upperTranslation line 232
  25. lemma OAI.CubicEisenstein.upperTranslation_section line 236
  26. theorem OAI.CubicEisenstein.upperEisenstein_periodic line 249
  27. lemma OAI.CubicEisenstein.integral_radial_sq line 261
  28. lemma OAI.CubicEisenstein.integrable_radial_sq_iff line 276
  29. lemma OAI.CubicEisenstein.add_one_image_Ioi line 283
  30. lemma OAI.CubicEisenstein.integrable_add_one_Ioi_iff line 294
  31. lemma OAI.CubicEisenstein.integral_add_one_Ioi line 304
  32. def OAI.CubicEisenstein.hyperbolicKernel line 314
  33. lemma OAI.CubicEisenstein.hyperbolicKernel_integrable line 316
  34. theorem OAI.CubicEisenstein.integral_hyperbolicKernel line 324
  35. lemma OAI.CubicEisenstein.breveE_norm line 340
  36. def OAI.CubicEisenstein.sourceFourierKernel line 347
  37. lemma OAI.CubicEisenstein.sourceFourierKernel_integrable line 350
  38. lemma OAI.CubicEisenstein.sourceFourierKernel_zero line 367
  39. lemma OAI.CubicEisenstein.sourceFrequency_inner line 372
  40. lemma OAI.CubicEisenstein.traceIntegral_eq_fourier line 378
  41. lemma OAI.CubicEisenstein.sourceFourierKernel_eq_fourier line 393
  42. lemma OAI.CubicEisenstein.hyperbolicKernel_laplace line 397
  43. lemma OAI.CubicEisenstein.source_gaussian_fourier line 409
  44. def OAI.CubicEisenstein.gaussianMixture line 419
  45. lemma OAI.CubicEisenstein.norm_gaussianMixture line 423
  46. lemma OAI.CubicEisenstein.gaussianMixture_slice_integrable line 431
  47. lemma OAI.CubicEisenstein.integral_norm_gaussianMixture line 445
  48. theorem OAI.CubicEisenstein.gaussianMixture_integrable line 461
  49. lemma OAI.CubicEisenstein.gaussianMixture_laplace_form line 485
  50. lemma OAI.CubicEisenstein.integral_gaussianMixture_t line 500
  51. lemma OAI.CubicEisenstein.integral_gaussianMixture_z line 506
  52. theorem OAI.CubicEisenstein.sourceFourierKernel_gamma line 527
  53. def OAI.CubicEisenstein.schlafliIntegral line 549
  54. lemma OAI.CubicEisenstein.schlafliIntegral_integrable line 553
  55. def OAI.CubicEisenstein.schlafliBesselK line 569
  56. lemma OAI.CubicEisenstein.sourceFourierKernel_gamma_schlafli line 572
  57. theorem OAI.CubicEisenstein.sourceFourierKernel_bessel line 584
  58. theorem OAI.CubicEisenstein.sourceFourierKernel_four_thirds line 608