OAI/NumberTheory/DirichletL/Eisenstein/CuspAverage.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.ramified_denominator_ne_zero line 81
  2. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_zero line 94
  3. lemma OAI.CubicEisenstein.cuspWhittakerHeightFactor_zero line 100
  4. lemma OAI.CubicEisenstein.opposite_zero_initial_cross line 108
  5. lemma OAI.CubicEisenstein.opposite_zero_cross_identity line 126
  6. theorem OAI.CubicEisenstein.translatedCuspFourier_opposite_zero_residue line 158
  7. lemma OAI.CubicEisenstein.rationalComplex_conjugate line 191
  8. lemma OAI.CubicEisenstein.hyperbolicEisenstein_rational_automorphy line 200
  9. lemma OAI.CubicEisenstein.hyperbolicEisenstein_rational_periodic line 207
  10. lemma OAI.CubicEisenstein.rationalComplex_unipotent_coe line 215
  11. lemma OAI.CubicEisenstein.rationalUnipotent_section line 223
  12. lemma OAI.CubicEisenstein.rationalComplex_T_pow_upper line 235
  13. theorem OAI.CubicEisenstein.rational_cusp_average_right_T line 242
  14. lemma OAI.CubicEisenstein.cuspFourierPhase_zero line 265
  15. lemma OAI.CubicEisenstein.kernelCuspFourier_zero line 268
  16. theorem OAI.CubicEisenstein.translatedCuspFourier_residue_eq_of_initial line 273
  17. lemma OAI.CubicEisenstein.sourceComplexMatrix_rationalLift line 318
  18. lemma OAI.CubicEisenstein.translatedCuspFourier_one_residue line 321
  19. lemma OAI.CubicEisenstein.translatedCuspFourier_bruhat_residue line 327
  20. theorem OAI.CubicEisenstein.kernelSourceProjection_residue_cusp_average line 351
  21. theorem OAI.CubicEisenstein.kernelSourceProjection_cubicEisensteinResidue_ne_zero line 363
  22. theorem OAI.CubicEisenstein.cubicSourceResidualFunction_cusp_average line 370
  23. theorem OAI.CubicEisenstein.cubicSourceResidualFunction_ne_zero line 378
  24. lemma OAI.CubicEisenstein.complex_gaussian_power_integrable line 393
  25. lemma OAI.CubicEisenstein.complex_gaussian_power_integral line 409
  26. def OAI.CubicEisenstein.cubicMellinMixture line 427
  27. lemma OAI.CubicEisenstein.cubicMellinMixture_slice_integrable line 431
  28. lemma OAI.CubicEisenstein.cubicMellinMixture_integral_x line 437
  29. lemma OAI.CubicEisenstein.cubicMellinMixture_norm line 463
  30. lemma OAI.CubicEisenstein.real_gaussian_power_integral line 475
  31. lemma OAI.CubicEisenstein.cubicMellinMixture_integral_norm line 482
  32. lemma OAI.CubicEisenstein.cubicMellinMixture_integrable line 510
  33. lemma OAI.CubicEisenstein.cubicMellinMixture_integral_t line 529
  34. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_mellin_mixture line 554
  35. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_mellin_integrable line 568
  36. lemma OAI.CubicEisenstein.cubicMellinMixture_double_integral line 576
  37. theorem OAI.CubicEisenstein.schlafliBesselK_cubic_mellin line 594