OAI/NumberTheory/DirichletL/Eisenstein/TranslatedFourierResidues.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.period_integral_fourier_translation line 86
  2. theorem OAI.CubicEisenstein.rational_cusp_fourier_right_T line 107
  3. lemma OAI.CubicEisenstein.translatedCuspFourier_residue_scaled_of_initial line 138
  4. lemma OAI.CubicEisenstein.translatedCuspFourier_one line 180
  5. lemma OAI.CubicEisenstein.translatedCuspFourier_bruhat line 185
  6. def OAI.CubicEisenstein.sourceRayPhaseSum line 211
  7. theorem OAI.CubicEisenstein.kernelSourceProjection_residue_fourier line 214
  8. lemma OAI.CubicEisenstein.sourceRayPhase_cube line 236
  9. lemma OAI.CubicEisenstein.sourceRayPhaseSum_formula line 242
  10. lemma OAI.CubicEisenstein.sourceRayPhaseSum_eq line 254
  11. lemma OAI.CubicEisenstein.kernelCuspFourier_residue_horizontal line 266
  12. lemma OAI.CubicEisenstein.kernelCuspFourier_residue_eq_zero_of_not_horizontal line 278
  13. theorem OAI.CubicEisenstein.kernelSourceProjection_residue_fourier_mask line 286
  14. lemma OAI.CubicEisenstein.oppositeFrequency_cross_identity line 303
  15. theorem OAI.CubicEisenstein.translatedCuspFourier_unramified_residue line 339
  16. def OAI.CubicEisenstein.principalArithmeticResidue line 370
  17. lemma OAI.CubicEisenstein.kernelCuspFourier_principal_residue line 373
  18. def OAI.CubicEisenstein.sourceArithmeticResidue line 385
  19. theorem OAI.CubicEisenstein.kernelSourceProjection_gauss_residue line 391
  20. theorem OAI.CubicEisenstein.cubicSourceResidualFunction_fourier_average line 402
  21. lemma OAI.CubicEisenstein.unramifiedGaussResidue_zero line 411
  22. lemma OAI.CubicEisenstein.sourceArithmeticResidue_zero line 421
  23. def OAI.CubicEisenstein.horizontalPhaseMultiplier line 435
  24. lemma OAI.CubicEisenstein.brevePhase_hasDerivAt line 438
  25. lemma OAI.CubicEisenstein.horizontalPhaseMultiplier_norm line 453
  26. lemma OAI.CubicEisenstein.horizontalPhaseMultiplier_wirtinger line 464
  27. lemma OAI.CubicEisenstein.norm_mul_exp_neg_bound line 473
  28. lemma OAI.CubicEisenstein.summable_norm_mul_exp_neg_cuspFrequency line 485
  29. def OAI.CubicEisenstein.cubicResidualDirectionalTerm line 493
  30. lemma OAI.CubicEisenstein.cubicResidualNonzeroTerm_horizontal_hasDerivAt line 496
  31. lemma OAI.CubicEisenstein.cubicResidualDirectionalTerm_slab_bound line 512
  32. lemma OAI.CubicEisenstein.cubicResidualDirectionalTerm_summable line 528
  33. lemma OAI.CubicEisenstein.cubicResidualNonzeroSeries_horizontal_hasDerivAt line 535
  34. lemma OAI.CubicEisenstein.cubicResidualFunction_horizontal_hasDerivAt line 546
  35. def OAI.CubicEisenstein.horizontalWirtingerBar line 563
  36. lemma OAI.CubicEisenstein.horizontalWirtingerBar_brevePhase line 567
  37. theorem OAI.CubicEisenstein.cubicResidualFunction_wirtingerBar line 576
  38. lemma OAI.CubicEisenstein.cubicResidualFunction_wirtingerBar_summable line 591