OAI/NumberTheory/DirichletL/GaussSum/SecondPoissonScale.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.second_prefactor_identity line 54
  2. theorem OAI.ActualEisensteinCubic.canonicalSextic_conj_as_row_label line 105
  3. theorem OAI.ActualEisensteinCubic.canonicalSextic_second_child line 134
  4. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_mul line 148
  5. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_conj_as_row_label line 156
  6. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_second_child line 169
  7. def OAI.ActualEisensteinCubic.rowCoprimeMask line 186
  8. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_self_pair line 191
  9. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_pair_kernel line 214
  10. theorem OAI.ActualEisensteinCubic.mask_powerset line 236
  11. theorem OAI.ActualEisensteinCubic.rowCoprimeMask_subsets line 270
  12. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_pair_sum_mobius line 278
  13. theorem OAI.ActualEisensteinCubic.finite_energy_expand line 314
  14. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_mean_square_mobius line 348
  15. theorem OAI.ActualEisensteinCubic.prime_product_moebius line 369
  16. theorem OAI.ActualEisensteinCubic.mem_prime_product_iff line 388
  17. def OAI.ConcretePrimeRowBridge.primeSubsetProduct line 407
  18. def OAI.ConcretePrimeRowBridge.residualSexticRow line 410
  19. theorem OAI.ConcretePrimeRowBridge.idealRowSum_mean_square_mobius line 420
  20. theorem OAI.ConcretePrimeRowBridge.idealSupport_product_dvd line 471
  21. theorem OAI.ConcretePrimeRowBridge.commonSupport_product_dvd line 485
  22. abbrev OAI.EisensteinSchwartzPoisson.LogPlane line 501
  23. theorem OAI.EisensteinSchwartzPoisson.fourier_prod_eq_iterated line 503
  24. def OAI.EisensteinSchwartzPoisson.complexPoint line 529
  25. theorem OAI.EisensteinSchwartzPoisson.complexPoint_eq line 531
  26. def OAI.EisensteinSchwartzPoisson.planeComplexIso line 534
  27. theorem OAI.EisensteinSchwartzPoisson.planeComplexIso_apply line 545
  28. theorem OAI.EisensteinSchwartzPoisson.horizontal_isometry line 548
  29. theorem OAI.EisensteinSchwartzPoisson.horizontal_temperate line 555
  30. def OAI.EisensteinSchwartzPoisson.horizontalSlice line 564
  31. theorem OAI.EisensteinSchwartzPoisson.horizontalSlice_apply line 568
  32. def OAI.EisensteinSchwartzPoisson.partialFourier line 571
  33. theorem OAI.EisensteinSchwartzPoisson.partialFourier_eq_integral line 574
  34. theorem OAI.EisensteinSchwartzPoisson.partialFourier_eq_exp_integral line 578
  35. def OAI.EisensteinSchwartzPoisson.verticalMajorant line 585
  36. theorem OAI.EisensteinSchwartzPoisson.verticalMajorant_integrable line 588
  37. theorem OAI.EisensteinSchwartzPoisson.norm_le_verticalMajorant line 591
  38. theorem OAI.EisensteinSchwartzPoisson.partialFourier_continuous line 604
  39. theorem OAI.EisensteinSchwartzPoisson.partialFourier_integrable line 625
  40. theorem OAI.EisensteinSchwartzPoisson.fourier_partialFourier line 640
  41. def OAI.EisensteinSchwartzPoisson.partialFourierSchwartz line 650
  42. theorem OAI.EisensteinSchwartzPoisson.partialFourierSchwartz_apply line 653
  43. theorem OAI.EisensteinSchwartzPoisson.partialFourierSchwartz_coe line 668
  44. theorem OAI.EisensteinSchwartzPoisson.fourier_partialFourierSchwartz line 672
  45. theorem OAI.EisensteinSchwartzPoisson.horizontal_hasFDerivAt line 677
  46. theorem OAI.EisensteinSchwartzPoisson.horizontalSlice_lineDerivOp line 686
  47. theorem OAI.EisensteinSchwartzPoisson.horizontalSlice_lineDerivOp_twice line 698
  48. theorem OAI.EisensteinSchwartzPoisson.summable_int_cauchy_weight line 703
  49. theorem OAI.EisensteinSchwartzPoisson.summable_int_cauchy_product line 719
  50. theorem OAI.EisensteinSchwartzPoisson.summable_norm_of_cauchy_product line 725
  51. theorem OAI.EisensteinSchwartzPoisson.summable_of_cauchy_product line 732
  52. def OAI.EisensteinSchwartzPoisson.planeDecayConstant line 737
  53. theorem OAI.EisensteinSchwartzPoisson.planeDecayConstant_nonneg line 741
  54. theorem OAI.EisensteinSchwartzPoisson.plane_schwartz_product_decay line 745
  55. theorem OAI.EisensteinSchwartzPoisson.norm_horizontalSlice_le line 769
  56. theorem OAI.EisensteinSchwartzPoisson.norm_inverse_horizontalSlice_le line 776
  57. theorem OAI.EisensteinSchwartzPoisson.norm_inverse_lineDeriv line 790
  58. theorem OAI.EisensteinSchwartzPoisson.sq_mul_norm_inverse_le_second line 801
  59. theorem OAI.EisensteinSchwartzPoisson.inverse_horizontalSlice_product_decay line 811
  60. def OAI.EisensteinSchwartzPoisson.partialFourierDecayConstant line 831
  61. theorem OAI.EisensteinSchwartzPoisson.partialFourierDecayConstant_nonneg line 835
  62. theorem OAI.EisensteinSchwartzPoisson.partialFourier_product_decay line 840
  63. theorem OAI.EisensteinSchwartzPoisson.norm_partialFourier_le line 846
  64. theorem OAI.EisensteinSchwartzPoisson.partialFourier_gaussian_summable_norm line 853
  65. theorem OAI.EisensteinSchwartzPoisson.partialFourier_gaussian_summable line 862
  66. theorem OAI.EisensteinSchwartzPoisson.plane_lattice_summable_norm line 866
  67. theorem OAI.EisensteinSchwartzPoisson.plane_lattice_summable line 875
  68. theorem OAI.EisensteinSchwartzPoisson.vertical_isometry line 879
  69. theorem OAI.EisensteinSchwartzPoisson.vertical_temperate line 887
  70. def OAI.EisensteinSchwartzPoisson.verticalSlice line 896
  71. theorem OAI.EisensteinSchwartzPoisson.verticalSlice_apply line 900
  72. theorem OAI.EisensteinSchwartzPoisson.schwartz_poisson_zero line 903
  73. theorem OAI.EisensteinSchwartzPoisson.vertical_poisson line 907
  74. theorem OAI.EisensteinSchwartzPoisson.horizontal_poisson line 912
  75. theorem OAI.EisensteinSchwartzPoisson.iterated_poisson_pair_sum line 919
  76. theorem OAI.EisensteinSchwartzPoisson.integer_pair_poisson line 935