OAI/NumberTheory/DirichletL/Eisenstein/BesselMellinTransform.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_scaled_mellin_integrable line 81
  2. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_scaled_mellin line 91
  3. lemma OAI.CubicEisenstein.source_cubic_bessel_mellin_integrable line 100
  4. theorem OAI.CubicEisenstein.source_cubic_bessel_mellin line 109
  5. theorem OAI.ShortDraftCRT.exists_fixed_completion line 133
  6. theorem OAI.ShortDraftCRT.fixed_completion_congr line 164
  7. lemma OAI.ShortDraftCRT.quotient_eq_of_dvd_sub line 190
  8. theorem OAI.ShortDraftCRT.fixed_completion_matrix_congr line 194
  9. theorem OAI.ShortDraftCRT.exists_fixed_matrix_completion line 215
  10. def OAI.CubicEisenstein.conductorReduction line 243
  11. lemma OAI.CubicEisenstein.conductorReduction_surjective line 247
  12. def OAI.CubicEisenstein.quotientTrace line 250
  13. lemma OAI.CubicEisenstein.quotientTrace_mk line 253
  14. def OAI.CubicEisenstein.conductorFourier line 261
  15. lemma OAI.CubicEisenstein.conductorFourier_shift line 266
  16. theorem OAI.CubicEisenstein.conductorFourier_support line 291
  17. lemma OAI.CubicEisenstein.conductorReduction_kernel_card line 308
  18. theorem OAI.CubicEisenstein.finite_tsum_conductor_pullback line 321
  19. lemma OAI.CubicEisenstein.quotientTrace_conductor_scale line 333
  20. theorem OAI.CubicEisenstein.conductorFourier_lift line 348
  21. lemma OAI.CubicEisenstein.cubicSymbol_pow_denominator line 375
  22. def OAI.CubicEisenstein.primeCubicMulChar line 381
  23. lemma OAI.CubicEisenstein.primeCubicMulChar_mk line 403
  24. lemma OAI.CubicEisenstein.quotientTrace_mk_product line 409
  25. lemma OAI.CubicEisenstein.conductorReduction_prime_power_unit line 418
  26. theorem OAI.CubicEisenstein.cubicUnitGaussSum_prime_power_fourier line 427
  27. theorem OAI.CubicEisenstein.cubicUnitGaussSum_prime_power_support line 459
  28. def OAI.CubicEisenstein.primeCubicGauss line 465
  29. theorem OAI.CubicEisenstein.cubicUnitGaussSum_prime_power_lift line 470
  30. lemma OAI.CubicEisenstein.primeCubicMulChar_cube line 486
  31. lemma OAI.CubicEisenstein.primeCubicMulChar_ne_one line 497
  32. lemma OAI.CubicEisenstein.primeCubicMulChar_order line 520
  33. lemma OAI.CubicEisenstein.primeCubicMulChar_pow_eq_one line 527
  34. lemma OAI.CubicEisenstein.primeCubicGauss_mod_three line 531
  35. lemma OAI.CubicEisenstein.primeCubicGauss_eq_gaussSum line 538
  36. theorem OAI.CubicEisenstein.primeCubicGauss_of_dvd line 545
  37. theorem OAI.CubicEisenstein.primeCubicGauss_trivial_nonzero line 562
  38. theorem OAI.CubicEisenstein.primeCubicGauss_one_mul_two line 575
  39. lemma OAI.CubicEisenstein.primeCubicGauss_one_eq line 598