OAI/NumberTheory/DirichletL/GaussSum/SexticRadialPoisson.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ActualEisensteinCubic.canonical_finite_prime_gauss_transform line 58
  2. def OAI.ActualEisensteinCubic.finiteSexticQuotientRow line 80
  3. theorem OAI.ActualEisensteinCubic.finiteSexticQuotientRow_one_mk line 89
  4. theorem OAI.ActualEisensteinCubic.finiteSexticQuotientRow_mk_eq_zero_iff line 100
  5. theorem OAI.ActualEisensteinCubic.canonical_finite_prime_gauss_transform_scalar line 114
  6. theorem OAI.ActualEisensteinCubic.finiteSexticQuotientRow_inv_eq_star line 132
  7. theorem OAI.ActualEisensteinCubic.canonical_finite_prime_gauss_transform_conj line 148
  8. theorem OAI.ActualEisensteinCubic.canonical_finite_prime_gauss_transform_vanishes line 163
  9. theorem OAI.ActualEisensteinCubic.finiteSexticQuotientRow_disjoint_pair_mk line 179
  10. theorem OAI.ActualEisensteinCubic.canonical_disjoint_pair_gauss_transform line 207
  11. def OAI.EisensteinSchwartzPoisson.paperE line 232
  12. def OAI.EisensteinSchwartzPoisson.paperFrequency line 234
  13. theorem OAI.EisensteinSchwartzPoisson.paperE_eq_exp line 237
  14. theorem OAI.EisensteinSchwartzPoisson.inner_paperFrequency line 241
  15. theorem OAI.EisensteinSchwartzPoisson.fourierChar_paperFrequency line 252
  16. theorem OAI.EisensteinSchwartzPoisson.dualFrequencyEquiv_coordinates line 259
  17. theorem OAI.EisensteinSchwartzPoisson.explicitDualFrequency_eq_paperFrequency line 267
  18. theorem OAI.EisensteinSchwartzPoisson.explicitDualFrequency_phase line 283
  19. theorem OAI.EisensteinSchwartzPoisson.paperFrequency_norm_sq line 290
  20. theorem OAI.EisensteinSchwartzPoisson.explicitDualFrequency_norm_sq line 298
  21. def OAI.EisensteinSchwartzPoisson.paperFourier line 304
  22. theorem OAI.EisensteinSchwartzPoisson.paperFourier_eq_standard line 307
  23. theorem OAI.EisensteinSchwartzPoisson.eisTraceModChar_eq_paperE line 320
  24. theorem OAI.EisensteinSchwartzPoisson.eisTraceModChar_frequency line 330
  25. theorem OAI.EisensteinSchwartzPoisson.actual_eisenstein_paper_poisson line 342
  26. theorem OAI.EisensteinSchwartzPoisson.actual_eisenstein_paper_poisson_trace line 387
  27. theorem OAI.EisensteinSchwartzPoisson.paperFourier_comp_mul line 406
  28. def OAI.EisensteinSchwartzPoisson.paperRadialFourier line 426
  29. theorem OAI.EisensteinSchwartzPoisson.paperFourier_radial line 429
  30. theorem OAI.EisensteinSchwartzPoisson.inverseSqrt_ne_zero line 452
  31. theorem OAI.EisensteinSchwartzPoisson.inverseSqrt_norm_sq line 456
  32. theorem OAI.EisensteinSchwartzPoisson.paperFourier_radial_scaled line 462
  33. def OAI.EisensteinSchwartzPoisson.scaledRadialTest line 481
  34. theorem OAI.EisensteinSchwartzPoisson.scaledRadialTest_apply line 485
  35. theorem OAI.EisensteinSchwartzPoisson.paperFourier_scaledRadialTest line 492
  36. theorem OAI.EisensteinSchwartzPoisson.actual_radial_paper_poisson_trace line 499
  37. theorem OAI.EisensteinSchwartzPoisson.actual_compact_radial_paper_poisson_trace line 541
  38. def OAI.ActualEisensteinCubic.finiteSexticRow line 562
  39. theorem OAI.ActualEisensteinCubic.finiteSexticRow_mul line 567
  40. theorem OAI.ActualEisensteinCubic.finite_prime_product_ne_bot line 574
  41. def OAI.ActualEisensteinCubic.finitePrimeModulus line 582
  42. theorem OAI.ActualEisensteinCubic.span_finitePrimeModulus line 585
  43. theorem OAI.ActualEisensteinCubic.finitePrimeModulus_ne_zero line 589
  44. theorem OAI.ActualEisensteinCubic.eisEmbedding_norm_sq_eq_absNorm_span line 597
  45. theorem OAI.ActualEisensteinCubic.finitePrimeModulus_norm_sq line 609
  46. def OAI.ActualEisensteinCubic.principalSexticRow line 614
  47. theorem OAI.ActualEisensteinCubic.principalSexticRow_mk line 622
  48. theorem OAI.ActualEisensteinCubic.canonical_principal_gauss_transform line 632
  49. theorem OAI.ActualEisensteinCubic.canonical_radial_poisson line 669
  50. def OAI.ActualEisensteinCubic.canonicalGaussSum line 713
  51. def OAI.ActualEisensteinCubic.canonicalNormalizedGauss line 726
  52. theorem OAI.ActualEisensteinCubic.canonical_radial_poisson_normalized line 732
  53. theorem OAI.ActualEisensteinCubic.canonical_compact_radial_poisson_normalized line 773
  54. theorem OAI.ActualEisensteinCubic.finiteSexticRow_eq_zero_iff line 789
  55. theorem OAI.ActualEisensteinCubic.finiteSexticRow_zero line 798
  56. theorem OAI.ActualEisensteinCubic.finiteSexticRow_radial_summable line 805
  57. theorem OAI.ActualEisensteinCubic.finiteSexticRow_disjoint_pair line 821
  58. theorem OAI.ActualEisensteinCubic.canonical_disjoint_pair_radial_poisson line 831