OAI/NumberTheory/DirichletL/Detector/GramPeriodicPoisson.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ProbeGramPeriodicPoisson.Joint line 13
  2. def OAI.ProbeGramPeriodicPoisson.point line 15
  3. def OAI.ProbeGramPeriodicPoisson.embeddingPair line 17
  4. theorem OAI.ProbeGramPeriodicPoisson.norm_point_sq line 20
  5. def OAI.ProbeGramPeriodicPoisson.leftInjection line 24
  6. def OAI.ProbeGramPeriodicPoisson.rightInjection line 28
  7. theorem OAI.ProbeGramPeriodicPoisson.point_eq_add line 32
  8. theorem OAI.ProbeGramPeriodicPoisson.slice_isometry line 38
  9. theorem OAI.ProbeGramPeriodicPoisson.slice_temperate line 44
  10. def OAI.ProbeGramPeriodicPoisson.leftSlice line 49
  11. theorem OAI.ProbeGramPeriodicPoisson.leftSlice_apply line 53
  12. theorem OAI.ProbeGramPeriodicPoisson.fourier_joint_eq_iterated line 56
  13. def OAI.ProbeGramPeriodicPoisson.partialFourier line 82
  14. def OAI.ProbeGramPeriodicPoisson.planeMajorant line 85
  15. theorem OAI.ProbeGramPeriodicPoisson.planeMajorant_integrable line 87
  16. def OAI.ProbeGramPeriodicPoisson.majorantConstant line 95
  17. theorem OAI.ProbeGramPeriodicPoisson.norm_le_planeMajorant line 99
  18. theorem OAI.ProbeGramPeriodicPoisson.partialFourier_continuous line 112
  19. theorem OAI.ProbeGramPeriodicPoisson.partialFourier_integrable line 129
  20. def OAI.ProbeGramPeriodicPoisson.partialFourierSchwartz line 143
  21. theorem OAI.ProbeGramPeriodicPoisson.partialFourierSchwartz_apply line 146
  22. theorem OAI.ProbeGramPeriodicPoisson.fourier_partialFourierSchwartz line 161
  23. theorem OAI.ProbeGramPeriodicPoisson.jointCLM_finite_seminorm_control line 165
  24. def OAI.ProbeGramPeriodicPoisson.productDecayConstant line 182
  25. theorem OAI.ProbeGramPeriodicPoisson.product_decay line 185
  26. theorem OAI.ProbeGramPeriodicPoisson.norm_le_product_majorant line 202
  27. theorem OAI.ProbeGramPeriodicPoisson.planeMajorant_eisenstein_summable line 208
  28. theorem OAI.ProbeGramPeriodicPoisson.joint_eisenstein_summable_norm line 225
  29. theorem OAI.ProbeGramPeriodicPoisson.joint_weighted_summable line 237
  30. theorem OAI.ProbeGramPeriodicPoisson.leftSlice_lineDeriv line 250
  31. theorem OAI.ProbeGramPeriodicPoisson.norm_inverse_lineDeriv line 264
  32. theorem OAI.ProbeGramPeriodicPoisson.inner_sq_mul_norm_inverse_le line 275
  33. theorem OAI.ProbeGramPeriodicPoisson.norm_sq_mul_norm_inverse_le line 284
  34. theorem OAI.ProbeGramPeriodicPoisson.norm_inverse_leftSlice_le line 296
  35. def OAI.ProbeGramPeriodicPoisson.leftSecondReal line 310
  36. def OAI.ProbeGramPeriodicPoisson.leftSecondImag line 313
  37. def OAI.ProbeGramPeriodicPoisson.sliceIntegralBound line 316
  38. def OAI.ProbeGramPeriodicPoisson.firstDecayBound line 319
  39. def OAI.ProbeGramPeriodicPoisson.secondDecayBound line 323
  40. theorem OAI.ProbeGramPeriodicPoisson.inverse_leftSlice_weight_le line 327
  41. theorem OAI.ProbeGramPeriodicPoisson.inverse_leftSlice_first_decay line 339
  42. theorem OAI.ProbeGramPeriodicPoisson.inverse_leftSlice_second_decay line 348
  43. theorem OAI.ProbeGramPeriodicPoisson.norm_partialFourier_le line 358
  44. theorem OAI.ProbeGramPeriodicPoisson.planeMajorant_cartesian_summable line 373
  45. def OAI.ProbeGramPeriodicPoisson.cartesianPoint line 386
  46. theorem OAI.ProbeGramPeriodicPoisson.joint_cartesian_summable_norm line 388
  47. theorem OAI.ProbeGramPeriodicPoisson.partialFourier_cartesian_summable_norm line 398
  48. theorem OAI.ProbeGramPeriodicPoisson.rightSlice_isometry line 408
  49. def OAI.ProbeGramPeriodicPoisson.rightSlice line 414
  50. theorem OAI.ProbeGramPeriodicPoisson.rightSlice_apply line 419
  51. theorem OAI.ProbeGramPeriodicPoisson.rightSlice_poisson line 422
  52. theorem OAI.ProbeGramPeriodicPoisson.joint_cartesian_eq_partial line 429
  53. theorem OAI.ProbeGramPeriodicPoisson.partial_cartesian_poisson line 445
  54. theorem OAI.ProbeGramPeriodicPoisson.cartesian_swap_tsum line 459
  55. theorem OAI.ProbeGramPeriodicPoisson.partial_cartesian_eq_fourier line 465
  56. theorem OAI.ProbeGramPeriodicPoisson.joint_cartesian_poisson line 471
  57. def OAI.ProbeGramPeriodicPoisson.blockMap line 476
  58. theorem OAI.ProbeGramPeriodicPoisson.blockMap_apply line 479
  59. theorem OAI.ProbeGramPeriodicPoisson.blockMap_symm_apply line 482
  60. theorem OAI.ProbeGramPeriodicPoisson.blockMap_det line 485
  61. def OAI.ProbeGramPeriodicPoisson.jointInverseJacobian line 494
  62. theorem OAI.ProbeGramPeriodicPoisson.jointInverseJacobian_blockMap line 497
  63. def OAI.ProbeGramPeriodicPoisson.jointDual line 502
  64. theorem OAI.ProbeGramPeriodicPoisson.joint_inner_linear_dual line 505
  65. theorem OAI.ProbeGramPeriodicPoisson.jointDual_blockMap line 510
  66. theorem OAI.ProbeGramPeriodicPoisson.joint_integral_comp_linearEquiv line 520
  67. theorem OAI.ProbeGramPeriodicPoisson.joint_fourier_comp_linearEquiv line 532
  68. def OAI.ProbeGramPeriodicPoisson.jointTranslate line 545
  69. def OAI.ProbeGramPeriodicPoisson.jointAffine line 549
  70. theorem OAI.ProbeGramPeriodicPoisson.jointAffine_apply line 552
  71. theorem OAI.ProbeGramPeriodicPoisson.joint_fourier_affine line 555
  72. theorem OAI.ProbeGramPeriodicPoisson.joint_affine_poisson line 569
  73. def OAI.ProbeGramPeriodicPoisson.jointFrequency line 581
  74. theorem OAI.ProbeGramPeriodicPoisson.actual_joint_coset_poisson line 586
  75. theorem OAI.ProbeGramPeriodicPoisson.joint_dual_summable_norm line 618
  76. theorem OAI.ProbeGramPeriodicPoisson.jointFrequency_summable_norm line 634
  77. abbrev OAI.ProbeGramPeriodicPoisson.Residue line 639
  78. def OAI.ProbeGramPeriodicPoisson.quotientPair line 641
  79. def OAI.ProbeGramPeriodicPoisson.representativePair line 644
  80. def OAI.ProbeGramPeriodicPoisson.jointFiberSplit line 647
  81. theorem OAI.ProbeGramPeriodicPoisson.joint_fiber_tsum line 656
  82. def OAI.ProbeGramPeriodicPoisson.residueFourier line 670
  83. theorem OAI.ProbeGramPeriodicPoisson.actual_joint_periodic_poisson line 676
  84. theorem OAI.ProbeGramPeriodicPoisson.actual_joint_periodic_fourier line 701
  85. theorem OAI.ProbeGramPeriodicPoisson.jointFrequency_zero line 727
  86. theorem OAI.ProbeGramPeriodicPoisson.residueFourier_zero line 732
  87. theorem OAI.ProbeGramPeriodicPoisson.residueFourier_norm_le line 737
  88. theorem OAI.ProbeGramPeriodicPoisson.principal_joint_inverse_covolume line 759
  89. theorem OAI.ProbeGramPeriodicPoisson.norm_periodic_zero_mean_le line 769
  90. def OAI.ProbeGramPeriodicPoisson.scaleMap line 818
  91. theorem OAI.ProbeGramPeriodicPoisson.scaleMap_apply line 822
  92. theorem OAI.ProbeGramPeriodicPoisson.scaleMap_dual line 827
  93. theorem OAI.ProbeGramPeriodicPoisson.scaleMap_inverseJacobian line 835
  94. def OAI.ProbeGramPeriodicPoisson.scaledSource line 842
  95. theorem OAI.ProbeGramPeriodicPoisson.scaledSource_apply line 845
  96. theorem OAI.ProbeGramPeriodicPoisson.fourier_scaledSource line 849
  97. theorem OAI.ProbeGramPeriodicPoisson.scaledSource_physicalPoint line 854
  98. def OAI.ProbeGramPeriodicPoisson.generatorRotation line 860
  99. theorem OAI.ProbeGramPeriodicPoisson.norm_generatorRotation line 862
  100. theorem OAI.ProbeGramPeriodicPoisson.scaled_jointFrequency_eq line 865
  101. theorem OAI.ProbeGramPeriodicPoisson.sqrt_ratio_decay line 885
  102. theorem OAI.ProbeGramPeriodicPoisson.physical_weighted_summable line 890
  103. theorem OAI.ProbeGramPeriodicPoisson.principal_high_bound line 900
  104. theorem OAI.ProbeGramPeriodicPoisson.norm_physical_weighted_le line 947
  105. theorem OAI.ProbeGramPeriodicPoisson.principal_periodic_bound line 961
  106. def OAI.ProbeGramPeriodicPoisson.idealQuotientPair line 1007
  107. theorem OAI.ProbeGramPeriodicPoisson.ideal_periodic_bound line 1010
  108. theorem OAI.ProbeGramPeriodicPoisson.principal_annular_periodic_bound line 1030
  109. theorem OAI.ProbeGramPeriodicPoisson.ideal_annular_periodic_bound line 1072