OAI/Analysis/CardinalInterpolation/ModTwelve.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

Modulo-twelve cardinal functions and Gaussian-damped radial Schwartz realization.

  1. abbrev OAI.Triangular.Plane line 13
  2. def OAI.Triangular.b line 15
  3. def OAI.Triangular.h line 17
  4. def OAI.Triangular.L line 19
  5. def OAI.Triangular.zeroSet line 21
  6. def OAI.Triangular.nodes line 24
  7. def OAI.Triangular.T line 26
  8. def OAI.Triangular.IsRadial line 28
  9. def OAI.Triangular.realFourier line 31
  10. lemma OAI.Triangular.b_pos line 34
  11. lemma OAI.Triangular.h_pos line 38
  12. lemma OAI.Triangular.b_sq line 40
  13. lemma OAI.Triangular.k_pos line 45
  14. lemma OAI.Triangular.hasDerivAt_T line 47
  15. lemma OAI.Triangular.deriv_T line 54
  16. lemma OAI.Triangular.T_pos line 58
  17. lemma OAI.Triangular.realFourier_eq_integral line 61
  18. lemma OAI.Triangular.zero_mem_zeroSet line 74
  19. lemma OAI.Triangular.twentyFour_mem_nodes line 77
  20. def OAI.Triangular.nodes₀ line 80
  21. abbrev OAI.Triangular.Node line 82
  22. lemma OAI.Triangular.Node.mem_zeroSet line 84
  23. def OAI.Triangular.Cardinal.sineFactor line 92
  24. def OAI.Triangular.Cardinal.rootProduct line 95
  25. def OAI.Triangular.Cardinal.P line 97
  26. lemma OAI.Triangular.Cardinal.P_eq_square line 99
  27. lemma OAI.Triangular.Cardinal.sineFactor_add_twelve line 102
  28. lemma OAI.Triangular.Cardinal.P_periodic line 112
  29. lemma OAI.Triangular.Cardinal.P_ofReal line 116
  30. lemma OAI.Triangular.Cardinal.P_nonneg line 122
  31. lemma OAI.Triangular.Cardinal.differentiable_rootProduct line 127
  32. lemma OAI.Triangular.Cardinal.differentiable_P line 131
  33. lemma OAI.Triangular.Cardinal.rootProduct_zero line 135
  34. lemma OAI.Triangular.Cardinal.P_zero line 148
  35. lemma OAI.Triangular.Cardinal.P_real_zero_iff line 152
  36. lemma OAI.Triangular.Cardinal.hasDerivAt_P_zero line 168
  37. lemma OAI.Triangular.Cardinal.deriv_P_zero line 174
  38. lemma OAI.Triangular.Cardinal.P_node line 177
  39. lemma OAI.Triangular.Cardinal.deriv_P_node line 179
  40. def OAI.Triangular.Cardinal.dBasis line 182
  41. def OAI.Triangular.Cardinal.cBasis line 184
  42. lemma OAI.Triangular.Cardinal.differentiable_dBasis line 186
  43. lemma OAI.Triangular.Cardinal.differentiable_cBasis line 191
  44. lemma OAI.Triangular.Cardinal.dBasis_node line 196
  45. lemma OAI.Triangular.Cardinal.dBasis_eq line 199
  46. lemma OAI.Triangular.Cardinal.cBasis_eq line 203
  47. lemma OAI.Triangular.Cardinal.node_cast_ne line 208
  48. lemma OAI.Triangular.Cardinal.dBasis_other line 212
  49. lemma OAI.Triangular.Cardinal.cBasis_other line 215
  50. lemma OAI.Triangular.Cardinal.mul_dBasis line 218
  51. lemma OAI.Triangular.Cardinal.mul_cBasis line 224
  52. lemma OAI.Triangular.Cardinal.deriv_dBasis_other line 230
  53. lemma OAI.Triangular.Cardinal.deriv_cBasis_other line 239
  54. lemma OAI.Triangular.Cardinal.cBasis_node line 248
  55. lemma OAI.Triangular.Cardinal.P_conj line 251
  56. lemma OAI.Triangular.Cardinal.dslope_conj_real line 255
  57. lemma OAI.Triangular.Cardinal.dBasis_conj line 274
  58. lemma OAI.Triangular.Cardinal.cBasis_conj line 278
  59. lemma OAI.Triangular.Cardinal.norm_two_sin_le line 282
  60. def OAI.Triangular.Cardinal.stripBound line 293
  61. lemma OAI.Triangular.Cardinal.stripBound_nonneg line 295
  62. lemma OAI.Triangular.Cardinal.P_strip_bound line 299
  63. lemma OAI.Triangular.Cardinal.im_le_dist_real line 320
  64. lemma OAI.Triangular.Cardinal.uniform_basis_bound line 323
  65. structure OAI.Triangular.Cardinal.Coefficients line 363
  66. def OAI.Triangular.Cardinal.profile line 369
  67. lemma OAI.Triangular.Cardinal.summand_norm_bound line 373
  68. lemma OAI.Triangular.Cardinal.differentiable_profile line 386
  69. lemma OAI.Triangular.Cardinal.profile_strip line 403
  70. lemma OAI.Triangular.Cardinal.profile_conj line 418
  71. lemma OAI.Triangular.Cardinal.profile_real line 423
  72. lemma OAI.Triangular.Cardinal.profile_eq line 428
  73. lemma OAI.Triangular.Cardinal.deriv_profile line 439
  74. lemma OAI.Triangular.Cardinal.profile_node line 465
  75. lemma OAI.Triangular.Cardinal.deriv_profile_node line 474
  76. lemma OAI.Triangular.Analysis.polynomial_gaussian_bound line 489
  77. lemma OAI.Triangular.Analysis.gaussian_schwartz_decay line 515
  78. def OAI.Triangular.Analysis.gaussianSchwartz line 544
  79. lemma OAI.Triangular.Analysis.gaussianSchwartz_apply line 549
  80. lemma OAI.Triangular.Analysis.iteratedDeriv_real_of_complex line 552
  81. lemma OAI.Triangular.Analysis.entire_real_temperate line 561
  82. def OAI.Triangular.Analysis.dampedEntireSchwartz line 576
  83. lemma OAI.Triangular.Analysis.dampedEntireSchwartz_apply line 580
  84. def OAI.Triangular.Cardinal.dampedProfile line 595
  85. lemma OAI.Triangular.Cardinal.dampedProfile_apply line 600
  86. lemma OAI.Triangular.Cardinal.dampedProfile_complex line 607
  87. lemma OAI.Triangular.Cardinal.dampedProfile_radial line 617
  88. theorem OAI.Triangular.Cardinal.cardinal_realization line 621