OAI/NumberTheory/DirichletL/Eisenstein/ResidualFourierExpansion.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.cubicResidualFullMode_density_integrable line 87
  2. lemma OAI.CubicEisenstein.cubicEisensteinResidue_slice_coefficient_ae line 107
  3. lemma OAI.CubicEisenstein.cubicEisensteinResidue_all_slice_coefficients_ae line 119
  4. lemma OAI.CubicEisenstein.cubicEisensteinResidue_all_fourier_integrals_ae line 126
  5. lemma OAI.CubicEisenstein.cubicResidualFunction_fourier_full line 145
  6. lemma OAI.CubicEisenstein.cubicResidualFunction_height_continuous line 155
  7. lemma OAI.CubicEisenstein.cubicResidualFunction_height_memLp line 162
  8. theorem OAI.CubicEisenstein.cubicEisensteinResidue_cell_slices_ae line 175
  9. theorem OAI.CubicEisenstein.cubicEisensteinResidue_cell_product_ae line 192
  10. lemma OAI.CubicEisenstein.periodDomain_memLp_of_continuous line 213
  11. lemma OAI.CubicEisenstein.upperTranslation_mem_kernel line 221
  12. lemma OAI.CubicEisenstein.kernelProjection_upper_period line 226
  13. lemma OAI.CubicEisenstein.ae_eq_of_periodDomain_eq line 237
  14. lemma OAI.CubicEisenstein.positive_height_interval_cover line 274
  15. lemma OAI.CubicEisenstein.hyperbolic_ae_of_coordinate_ae line 293
  16. lemma OAI.CubicEisenstein.hyperbolic_eq_ae_of_period_cells line 318
  17. theorem OAI.CubicEisenstein.cubicEisensteinResidue_continuous_representative line 352
  18. lemma OAI.CubicEisenstein.kernelProjection_quasiMeasurePreserving line 370
  19. lemma OAI.CubicEisenstein.kernelLevel_character_ae_on_hyperbolic line 395
  20. lemma OAI.CubicEisenstein.kernelLevel_character_continuous_representative line 412
  21. theorem OAI.CubicEisenstein.cubicResidualFunction_automorphy line 438
  22. lemma OAI.CubicEisenstein.cubicResidualFunction_ne_zero line 445
  23. lemma OAI.CubicEisenstein.cubicResidualFunction_exists_ne_zero line 458
  24. lemma OAI.CubicEisenstein.sourceProjection_continuous line 466
  25. lemma OAI.CubicEisenstein.sourceProjection_congr_ae line 474
  26. lemma OAI.CubicEisenstein.kernelSourceProjection_hyperbolic_representative line 486
  27. def OAI.CubicEisenstein.cubicSourceResidualFunction line 499
  28. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_continuous line 501
  29. theorem OAI.CubicEisenstein.cubicSourceResidualFunction_automorphy line 504
  30. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_rational_invariant line 509
  31. theorem OAI.CubicEisenstein.cubicSourceResidualFunction_represents_projection line 516
  32. def OAI.CubicEisenstein.rationalUnipotent line 531
  33. lemma OAI.CubicEisenstein.rationalUnipotent_add line 534
  34. lemma OAI.CubicEisenstein.rationalUnipotent_zero line 543
  35. lemma OAI.CubicEisenstein.rationalUnipotent_neg line 548
  36. lemma OAI.CubicEisenstein.rationalUnipotent_one line 552
  37. lemma OAI.CubicEisenstein.row_unipotent_conjugate line 554
  38. def OAI.CubicEisenstein.cuspUnipotentTranslate line 573
  39. lemma OAI.CubicEisenstein.cuspUnipotentTranslate_inverse line 579
  40. def OAI.CubicEisenstein.cuspUnipotentEquiv line 588
  41. lemma OAI.CubicEisenstein.cosetRow_cuspUnipotentEquiv line 594
  42. lemma OAI.CubicEisenstein.cosetCharacter_cuspUnipotentEquiv line 600
  43. lemma OAI.CubicEisenstein.embeddedRow_cuspUnipotentEquiv line 605
  44. lemma OAI.CubicEisenstein.summand_unipotent line 612
  45. theorem OAI.CubicEisenstein.eisenstein_unipotent line 618
  46. theorem OAI.CubicEisenstein.hyperbolicEisenstein_unipotent line 624