OAI/NumberTheory/DirichletL/Eisenstein/FourierCoefficients.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.breveE_embedding_div_traceLambda line 82
  2. def OAI.CubicEisenstein.cuspFrequency line 87
  3. lemma OAI.CubicEisenstein.cuspFrequency_period line 89
  4. lemma OAI.CubicEisenstein.cuspFrequency_negative_period line 97
  5. lemma OAI.CubicEisenstein.trace_mul_integrable line 105
  6. lemma OAI.CubicEisenstein.integrableOn_periodization line 114
  7. theorem OAI.CubicEisenstein.integral_fourier_periodization line 126
  8. lemma OAI.CubicEisenstein.continuous_inverse_upper_operator line 147
  9. lemma OAI.CubicEisenstein.continuous_upper_rowBound line 157
  10. lemma OAI.CubicEisenstein.norm_mem_periodDomain line 161
  11. lemma OAI.CubicEisenstein.exists_upper_rowBound line 166
  12. lemma OAI.CubicEisenstein.continuous_upper_summand line 176
  13. lemma OAI.CubicEisenstein.upper_summable_majorant line 192
  14. lemma OAI.CubicEisenstein.periodDomain_finiteMeasure line 208
  15. theorem OAI.CubicEisenstein.hasSum_integral_upperEisenstein line 213
  16. theorem OAI.CubicEisenstein.integral_upperEisenstein_eq_sum line 237
  17. def OAI.CubicEisenstein.shiftedHeightKernel line 251
  18. lemma OAI.CubicEisenstein.shiftedHeightKernel_integrable line 254
  19. lemma OAI.CubicEisenstein.primitiveTerm_eq_shiftedHeightKernel line 261
  20. lemma OAI.CubicEisenstein.primitiveTerm_integrable line 281
  21. lemma OAI.CubicEisenstein.traceIntegral_translate line 286
  22. lemma OAI.CubicEisenstein.traceIntegral_scale line 298
  23. lemma OAI.CubicEisenstein.traceIntegral_shiftedHeightKernel line 312
  24. lemma OAI.CubicEisenstein.period_integral_translation line 334
  25. lemma OAI.CubicEisenstein.breveE_quarter_eq_neg_one line 347
  26. lemma OAI.CubicEisenstein.cuspFrequency_ne_zero line 352
  27. theorem OAI.CubicEisenstein.integral_cusp_character line 355
  28. def OAI.CubicEisenstein.primitiveRowIntegral line 386
  29. lemma OAI.CubicEisenstein.integral_summand_eq_primitiveRowIntegral line 389
  30. lemma OAI.CubicEisenstein.hasSum_primitiveRowIntegrals line 399
  31. lemma OAI.CubicEisenstein.primitiveRowIntegral_sum_translate line 408
  32. lemma OAI.CubicEisenstein.primitiveTerm_fourier_integral line 422
  33. def OAI.CubicEisenstein.arithmeticResidueSum line 432
  34. lemma OAI.CubicEisenstein.arithmeticResidueSum_finite line 436
  35. lemma OAI.CubicEisenstein.denominator_integral_formula line 444
  36. instance OAI.CubicEisenstein.(instance at line 474) line 474
  37. instance OAI.CubicEisenstein.(instance at line 475) line 475
  38. lemma OAI.CubicEisenstein.summable_embedding_rpow line 477
  39. lemma OAI.CubicEisenstein.norm_row_symbol line 491
  40. lemma OAI.CubicEisenstein.norm_arithmeticResidueSum_le line 503
  41. def OAI.CubicEisenstein.arithmeticDirichletTerm line 527
  42. lemma OAI.CubicEisenstein.norm_arithmeticDirichletTerm_le line 530
  43. theorem OAI.CubicEisenstein.arithmeticDirichletTerm_summable_norm line 548
  44. def OAI.CubicEisenstein.arithmeticDirichletSeries line 555
  45. def OAI.CubicEisenstein.scatteringCoefficient line 558
  46. lemma OAI.CubicEisenstein.zero_lower_integral line 568
  47. lemma OAI.CubicEisenstein.integral_upperEisenstein_arithmetic line 580
  48. def OAI.CubicEisenstein.eisensteinFourierCoefficient line 611
  49. theorem OAI.CubicEisenstein.eisensteinFourierCoefficient_formula line 615
  50. theorem OAI.CubicEisenstein.eisensteinConstantCoefficient_formula line 622
  51. theorem OAI.CubicEisenstein.eisensteinFourierCoefficient_bessel line 629