OAI/NumberTheory/DirichletL/Eisenstein/OppositeCusp.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CubicEisenstein.PrimaryLower line 85
  2. abbrev OAI.CubicEisenstein.OppositeData line 86
  3. lemma OAI.CubicEisenstein.primaryLower_primary line 88
  4. lemma OAI.CubicEisenstein.primaryLower_ne_zero line 89
  5. def OAI.CubicEisenstein.oppositeDataToPrimitive line 91
  6. lemma OAI.CubicEisenstein.oppositeDataToPrimitive_bijective line 98
  7. def OAI.CubicEisenstein.oppositeDataEquiv line 125
  8. def OAI.CubicEisenstein.oppositeMatrix line 128
  9. lemma OAI.CubicEisenstein.rowOperator_opposite line 130
  10. def OAI.CubicEisenstein.oppositeEisenstein line 135
  11. lemma OAI.CubicEisenstein.rowHeight_eq_shiftedHeightKernel line 138
  12. def OAI.CubicEisenstein.oppositeTerm line 157
  13. lemma OAI.CubicEisenstein.oppositeTerm_eq_shifted line 161
  14. lemma OAI.CubicEisenstein.opposite_summand line 169
  15. theorem OAI.CubicEisenstein.oppositeEisenstein_eq_rows line 198
  16. theorem OAI.CubicEisenstein.opposite_rows_summable_norm line 204
  17. def OAI.CubicEisenstein.primaryLowerIdealEquiv line 210
  18. abbrev OAI.CubicEisenstein.CoprimeElement line 225
  19. def OAI.CubicEisenstein.cubicResidueElementMap line 227
  20. lemma OAI.CubicEisenstein.cubicResidueElementMap_bijective line 235
  21. def OAI.CubicEisenstein.cubicResidueElementEquiv line 266
  22. lemma OAI.CubicEisenstein.oppositeTerm_shift line 270
  23. def OAI.CubicEisenstein.oppositeGaussSum line 279
  24. theorem OAI.CubicEisenstein.oppositeGaussSum_eq line 284
  25. def OAI.CubicEisenstein.oppositeArithmeticSeries line 307
  26. theorem OAI.CubicEisenstein.oppositeArithmeticSeries_eq line 310
  27. lemma OAI.CubicEisenstein.continuous_inverse_fixed_left_operator line 329
  28. lemma OAI.CubicEisenstein.exists_fixed_left_rowBound line 338
  29. lemma OAI.CubicEisenstein.continuous_fixed_left_summand line 349
  30. lemma OAI.CubicEisenstein.fixed_left_summable_majorant line 364
  31. theorem OAI.CubicEisenstein.hasSum_integral_fixed_left_Eisenstein line 381
  32. def OAI.CubicEisenstein.oppositeIntegral line 412
  33. theorem OAI.CubicEisenstein.hasSum_oppositeIntegrals line 415
  34. lemma OAI.CubicEisenstein.oppositeTerm_integrable line 427
  35. lemma OAI.CubicEisenstein.oppositeIntegral_sum_translate line 432
  36. lemma OAI.CubicEisenstein.oppositeTerm_fourier_integral line 446
  37. lemma OAI.CubicEisenstein.oppositeDenominator_integral_formula line 458
  38. lemma OAI.CubicEisenstein.unramifiedCubicGaussSeries_twentySeven line 481
  39. theorem OAI.CubicEisenstein.oppositeEisenstein_fourier line 491
  40. theorem OAI.CubicEisenstein.oppositeEisenstein_fourier_unramified line 508
  41. abbrev OAI.CubicEisenstein.PeriodTorusL2 line 532
  42. def OAI.CubicEisenstein.periodIocCube line 534
  43. def OAI.CubicEisenstein.periodCovolumeDensity line 536
  44. lemma OAI.CubicEisenstein.periodCovolumeDensity_ne_zero line 538
  45. lemma OAI.CubicEisenstein.periodIocCube_measurable line 541
  46. lemma OAI.CubicEisenstein.periodIocCube_ae line 544
  47. def OAI.CubicEisenstein.periodSection line 547
  48. lemma OAI.CubicEisenstein.periodSection_measurableEmbedding line 550
  49. lemma OAI.CubicEisenstein.periodTorus_measurable line 555
  50. lemma OAI.CubicEisenstein.periodTorus_section line 561
  51. lemma OAI.CubicEisenstein.periodVector_Ioc_measurePreserving line 565
  52. lemma OAI.CubicEisenstein.periodSection_measurePreserving line 574
  53. lemma OAI.CubicEisenstein.periodTorus_measurePreserving line 581
  54. lemma OAI.CubicEisenstein.periodSection_torus_ae line 589
  55. lemma OAI.CubicEisenstein.periodSection_memLp line 596
  56. def OAI.CubicEisenstein.periodTorusL2Lift line 601
  57. lemma OAI.CubicEisenstein.periodTorusL2Lift_ae line 604
  58. lemma OAI.CubicEisenstein.periodTorusL2Lift_pullback line 608
  59. lemma OAI.CubicEisenstein.periodTorusL2Lift_frequency_integral line 617
  60. lemma OAI.CubicEisenstein.periodTorusL2Lift_fourierCoeff line 626
  61. theorem OAI.CubicEisenstein.periodDomain_L2_ext line 636