OAI/Analysis/PlanarPacking/Entire.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

Gaussian cardinal interpolation

The folded spectral representation gives the cardinal values and derivatives. Gaussian damping then extends the radial cardinal functions to Schwartz functions.

  1. lemma OAI.SharpPlanar.weighted_exp_integral line 30
  2. lemma OAI.SharpPlanar.exponential_division_one line 51
  3. lemma OAI.SharpPlanar.exponential_division_two line 65
  4. lemma OAI.SharpPlanar.triangular_piece_integrals line 86
  5. def OAI.SharpPlanar.foldedU line 127
  6. def OAI.SharpPlanar.foldedV line 131
  7. lemma OAI.SharpPlanar.u_integrand line 135
  8. lemma OAI.SharpPlanar.v_integrand line 160
  9. lemma OAI.SharpPlanar.P_as_table line 188
  10. lemma OAI.SharpPlanar.polynomial_reduce line 199
  11. lemma OAI.SharpPlanar.P_cos_factor line 211
  12. lemma OAI.SharpPlanar.phase_nat line 227
  13. lemma OAI.SharpPlanar.polynomial_fourier_algebra line 234
  14. theorem OAI.SharpPlanar.P_fourier line 250
  15. def OAI.SharpPlanar.Pmoment line 261
  16. lemma OAI.SharpPlanar.Pmoment_zero line 266
  17. lemma OAI.SharpPlanar.Pmoment_hasDerivAt line 270
  18. lemma OAI.SharpPlanar.trig_nat_mod12 line 286
  19. lemma OAI.SharpPlanar.Pmoment_mod line 297
  20. lemma OAI.SharpPlanar.phase_node line 304
  21. lemma OAI.SharpPlanar.Pmoment_node_formula line 311
  22. lemma OAI.SharpPlanar.Pmoment_node_0 line 319
  23. lemma OAI.SharpPlanar.Pmoment_node_1 line 329
  24. lemma OAI.SharpPlanar.Pmoment_node_3 line 341
  25. lemma OAI.SharpPlanar.Pmoment_node_4 line 353
  26. lemma OAI.SharpPlanar.Pmoment_node_7 line 365
  27. lemma OAI.SharpPlanar.Pmoment_node_9 line 377
  28. theorem OAI.SharpPlanar.Pmoment_node_data line 390
  29. lemma OAI.SharpPlanar.foldedU_unfold line 408
  30. lemma OAI.SharpPlanar.foldedV_unfold line 422
  31. lemma OAI.SharpPlanar.foldedU_divided line 435
  32. lemma OAI.SharpPlanar.foldedV_divided line 454
  33. lemma OAI.SharpPlanar.exp_phase_split line 469
  34. lemma OAI.SharpPlanar.foldedU_quotient line 477
  35. lemma OAI.SharpPlanar.foldedV_quotient line 507
  36. lemma OAI.SharpPlanar.folded_basis_quotients line 530
  37. lemma OAI.SharpPlanar.fourierIntegral_temperate line 546
  38. def OAI.SharpPlanar.spectral line 558
  39. def OAI.SharpPlanar.spectralForm line 561
  40. lemma OAI.SharpPlanar.spectral_eq line 564
  41. lemma OAI.SharpPlanar.spectral_temperate line 579
  42. lemma OAI.SharpPlanar.integrable_moment_Icc line 585
  43. lemma OAI.SharpPlanar.spectral_Icc_temperate line 591
  44. lemma OAI.SharpPlanar.spectral_integrable line 600
  45. lemma OAI.SharpPlanar.spectral_hasDerivAt line 610
  46. lemma OAI.SharpPlanar.interval_spectral_eq line 643
  47. lemma OAI.SharpPlanar.interval_exponential_hasDerivAt line 656
  48. def OAI.SharpPlanar.basisMoment line 676
  49. lemma OAI.SharpPlanar.basisMoment_zero line 681
  50. lemma OAI.SharpPlanar.basisMoment_hasDerivAt line 685
  51. lemma OAI.SharpPlanar.basisU_factor line 704
  52. lemma OAI.SharpPlanar.basisV_factor line 715
  53. lemma OAI.SharpPlanar.P_hasDerivAt line 727
  54. lemma OAI.SharpPlanar.basisU_factor_deriv1 line 730
  55. lemma OAI.SharpPlanar.basisU_factor_deriv2 line 740
  56. lemma OAI.SharpPlanar.basisU_factor_deriv3 line 752
  57. lemma OAI.SharpPlanar.basisV_factor_deriv1 line 766
  58. lemma OAI.SharpPlanar.basisV_factor_deriv2 line 775
  59. theorem OAI.SharpPlanar.basis_diagonal_jets line 786
  60. theorem OAI.SharpPlanar.basis_off_diagonal_jets line 799
  61. lemma OAI.SharpPlanar.realSpectral_norm line 823
  62. lemma OAI.SharpPlanar.basisMoment_bound line 834
  63. def OAI.SharpPlanar.cardinalSeries line 865
  64. lemma OAI.SharpPlanar.cardinalSeries_summand_bound line 870
  65. lemma OAI.SharpPlanar.cardinalSeries_summable line 884
  66. lemma OAI.SharpPlanar.cardinalSeries_hasDerivAt line 890
  67. lemma OAI.SharpPlanar.cardinalSeries_jets line 903
  68. lemma OAI.SharpPlanar.cardinalSeries_origin_jets line 938
  69. lemma OAI.SharpPlanar.interval_integral_tsum_uniform line 972
  70. def OAI.SharpPlanar.directKernel line 990
  71. lemma OAI.SharpPlanar.continuous_directKernel line 993
  72. lemma OAI.SharpPlanar.directDensity_tsum line 997
  73. lemma OAI.SharpPlanar.direct_piece_integrable line 1027
  74. lemma OAI.SharpPlanar.basis_piece_integrable line 1033
  75. lemma OAI.SharpPlanar.direct_basis_pair line 1041
  76. lemma OAI.SharpPlanar.direct_basis_integral_bound line 1054
  77. lemma OAI.SharpPlanar.direct_basis_integral_summable line 1073
  78. lemma OAI.SharpPlanar.direct_positive_series line 1079
  79. def OAI.SharpPlanar.expCut line 1107
  80. lemma OAI.SharpPlanar.expCut_smooth line 1110
  81. lemma OAI.SharpPlanar.expCut_eq line 1114
  82. lemma OAI.SharpPlanar.expCut_zero line 1117
  83. lemma OAI.SharpPlanar.iteratedDeriv_expCut_pos line 1120
  84. lemma OAI.SharpPlanar.iteratedDeriv_expCut_neg line 1127
  85. lemma OAI.SharpPlanar.expCut_decay line 1135
  86. def OAI.SharpPlanar.expCutSchwartz line 1162
  87. def OAI.SharpPlanar.gaussianSchwartz line 1170
  88. lemma OAI.SharpPlanar.gaussianSchwartz_apply line 1176
  89. lemma OAI.SharpPlanar.spectral_dirac_eq line 1188
  90. lemma OAI.SharpPlanar.spectral_dirac_temperate line 1193
  91. def OAI.SharpPlanar.cardinal line 1201
  92. lemma OAI.SharpPlanar.cardinal_temperate line 1209
  93. lemma OAI.SharpPlanar.radiusCoord_temperate line 1230
  94. def OAI.SharpPlanar.qSchwartz line 1234
  95. lemma OAI.SharpPlanar.qSchwartz_apply line 1238
  96. lemma OAI.SharpPlanar.directDensity_split line 1253
  97. lemma OAI.SharpPlanar.directDensity_series line 1270
  98. lemma OAI.SharpPlanar.spectral_interval_direct line 1283
  99. lemma OAI.SharpPlanar.cardinal_eq_cardinalSeries line 1296
  100. lemma OAI.SharpPlanar.cardinal_hasDerivAt line 1320
  101. lemma OAI.SharpPlanar.cardinal_jets line 1324