OAI/Analysis/Fourier/SphereExtension.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

Fourier extension from the unit sphere in the fourth-power range.

  1. abbrev OAI.EllipticCapacity.Space line 13
  2. abbrev OAI.EllipticCapacity.Sphere line 14
  3. def OAI.EllipticCapacity.surfaceArea line 16
  4. def OAI.EllipticCapacity.extension line 18
  5. def OAI.EllipticCapacity.SphereRestriction line 22
  6. theorem OAI.EllipticCapacity.surfaceArea_univ line 28
  7. theorem OAI.EllipticCapacity.kernel_norm line 39
  8. instance OAI.EllipticCapacity.surfaceArea_isFiniteMeasure line 45
  9. theorem OAI.EllipticCapacity.extension_integrable line 50
  10. theorem OAI.EllipticCapacity.extension_norm_le line 60
  11. theorem OAI.EllipticCapacity.extension_continuous line 71
  12. theorem OAI.EllipticCapacity.norm_exp_mul_I_sub_le line 83
  13. theorem OAI.EllipticCapacity.kernel_norm_sub_le line 99
  14. theorem OAI.EllipticCapacity.extension_norm_sub_le line 119
  15. def OAI.EllipticCapacity.SphereFourthPower line 142
  16. def OAI.EllipticCapacity.character line 147
  17. lemma OAI.EllipticCapacity.character_norm line 150
  18. lemma OAI.EllipticCapacity.character_add line 152
  19. lemma OAI.EllipticCapacity.character_neg line 154
  20. abbrev OAI.EllipticCapacity.Quad line 158
  21. def OAI.EllipticCapacity.quadMeasure line 159
  22. instance OAI.EllipticCapacity.(instance at line 160) line 160
  23. def OAI.EllipticCapacity.quadVector line 161
  24. def OAI.EllipticCapacity.quadAmplitude line 162
  25. lemma OAI.EllipticCapacity.quad_character line 164
  26. lemma OAI.EllipticCapacity.fourth_power_expansion line 169
  27. lemma OAI.EllipticCapacity.quadAmplitude_bound line 201
  28. def OAI.EllipticCapacity.gaussian line 209
  29. def OAI.EllipticCapacity.heatKernel line 210
  30. lemma OAI.EllipticCapacity.gaussian_pos line 213
  31. lemma OAI.EllipticCapacity.heatKernel_nonneg line 214
  32. lemma OAI.EllipticCapacity.gaussian_integrable line 218
  33. lemma OAI.EllipticCapacity.gaussian_character_integral line 224
  34. lemma OAI.EllipticCapacity.gaussian_quad_integrable line 243
  35. lemma OAI.EllipticCapacity.gaussian_fourth_identity line 255
  36. lemma OAI.EllipticCapacity.heatKernel_integrable line 270
  37. lemma OAI.EllipticCapacity.gaussian_fourth_integrable line 283
  38. lemma OAI.EllipticCapacity.gaussian_fourth_bound line 292
  39. lemma OAI.EllipticCapacity.gaussian_le_one line 323
  40. lemma OAI.EllipticCapacity.lintegral_gaussian_fourth_bound line 328
  41. lemma OAI.EllipticCapacity.fourth_power_majorant line 345
  42. lemma OAI.EllipticCapacity.integral_polar_three line 375
  43. abbrev OAI.EllipticCapacity.CrossPlane line 419
  44. def OAI.EllipticCapacity.sphereSplit line 421
  45. lemma OAI.EllipticCapacity.sphereSplit_measurePreserving line 426
  46. lemma OAI.EllipticCapacity.sphereSplit_symm_apply line 437
  47. lemma OAI.EllipticCapacity.sphereSplit_norm_sq line 442
  48. def OAI.EllipticCapacity.sphereKernel line 448
  49. def OAI.EllipticCapacity.ballFourier line 451
  50. lemma OAI.EllipticCapacity.ballFourier_polar line 454
  51. lemma OAI.EllipticCapacity.sphereSplit_symm_first line 498
  52. lemma OAI.EllipticCapacity.sphereSplit_ball_slice line 503
  53. lemma OAI.EllipticCapacity.plane_slice_volume line 513
  54. lemma OAI.EllipticCapacity.integral_ball_head line 531
  55. lemma OAI.EllipticCapacity.hasDerivAt_symmetric_integral line 581
  56. lemma OAI.EllipticCapacity.hasDerivAt_weighted_slice line 595
  57. lemma OAI.EllipticCapacity.ballFourier_hasDerivAt_one line 614
  58. lemma OAI.EllipticCapacity.ballFourier_isometry line 629
  59. lemma OAI.EllipticCapacity.extension_one_isometry line 650
  60. def OAI.EllipticCapacity.spaceAxis line 657
  61. lemma OAI.EllipticCapacity.spaceAxis_norm line 659
  62. lemma OAI.EllipticCapacity.spaceAxis_inner line 662
  63. lemma OAI.EllipticCapacity.extension_one_axis line 665
  64. lemma OAI.EllipticCapacity.extension_one_axis_formula line 690
  65. theorem OAI.EllipticCapacity.extension_one_formula line 704
  66. def OAI.EllipticCapacity.box line 718
  67. lemma OAI.EllipticCapacity.box_measurable line 720
  68. lemma OAI.EllipticCapacity.box_bound line 722
  69. lemma OAI.EllipticCapacity.box_integrable line 725
  70. lemma OAI.EllipticCapacity.box_integral line 729
  71. lemma OAI.EllipticCapacity.box_neg line 734
  72. lemma OAI.EllipticCapacity.box_mul_self line 740
  73. lemma OAI.EllipticCapacity.box_fourier line 743
  74. lemma OAI.EllipticCapacity.box_fourier_continuous line 769
  75. lemma OAI.EllipticCapacity.box_norm_integral line 773
  76. lemma OAI.EllipticCapacity.box_fourier_bound line 778
  77. lemma OAI.EllipticCapacity.box_fourier_decay line 782
  78. lemma OAI.EllipticCapacity.box_fourier_sq_integrable line 790
  79. def OAI.EllipticCapacity.tent line 813
  80. lemma OAI.EllipticCapacity.tent_integrable line 815
  81. lemma OAI.EllipticCapacity.tent_fourier line 818
  82. lemma OAI.EllipticCapacity.tent_fourier_integrable line 821
  83. lemma OAI.EllipticCapacity.tent_zero line 826
  84. lemma OAI.EllipticCapacity.tent_continuousAt_zero line 830
  85. lemma OAI.EllipticCapacity.integral_box_fourier_sq line 854
  86. def OAI.EllipticCapacity.sineSq line 858
  87. def OAI.EllipticCapacity.sineFourth line 860
  88. lemma OAI.EllipticCapacity.sineSq_fourier_ae line 862
  89. lemma OAI.EllipticCapacity.sineSq_integrable line 870
  90. lemma OAI.EllipticCapacity.sineSq_integral line 875
  91. lemma OAI.EllipticCapacity.sineFourth_identity line 883
  92. lemma OAI.EllipticCapacity.sineFourth_integrable line 892
  93. lemma OAI.EllipticCapacity.sineFourth_integral line 898
  94. lemma OAI.EllipticCapacity.sineFourth_abs line 906
  95. lemma OAI.EllipticCapacity.sineFourth_integral_Ioi line 912
  96. lemma OAI.EllipticCapacity.fourth_radial_density line 917
  97. lemma OAI.EllipticCapacity.extension_one_fourth_ae line 923
  98. lemma OAI.EllipticCapacity.extension_one_fourth_integrable line 930
  99. lemma OAI.EllipticCapacity.extension_one_fourth_integral line 943
  100. lemma OAI.EllipticCapacity.extension_one_fourth_lintegral line 957
  101. lemma OAI.EllipticCapacity.extension_congr_ae line 963
  102. lemma OAI.EllipticCapacity.eLpNorm_fourth_power line 970
  103. theorem OAI.EllipticCapacity.sphere_fourth_power line 982
  104. lemma OAI.EllipticCapacity.extension_enorm_le_essSup line 1016
  105. theorem OAI.EllipticCapacity.sphere_restriction_ge_four line 1030