OAI/Analysis/PlanarEndpoint/Fourier.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. abbrev OAI.PlanarEndpoint.Plane line 13
  2. abbrev OAI.PlanarEndpoint.L2 line 14
  3. def OAI.PlanarEndpoint.fourier line 16
  4. def OAI.PlanarEndpoint.InHThird line 19
  5. def OAI.PlanarEndpoint.hThirdNorm line 23
  6. def OAI.PlanarEndpoint.abel line 27
  7. def OAI.PlanarEndpoint.diskAverage line 32
  8. def OAI.PlanarEndpoint.lebesgueRepresentative line 35
  9. def OAI.PlanarEndpoint.IsLebesguePoint line 38
  10. def OAI.PlanarEndpoint.MainConclusion line 43
  11. lemma OAI.PlanarEndpoint.fourier_memLp line 60
  12. def OAI.PlanarEndpoint.phase line 69
  13. lemma OAI.PlanarEndpoint.norm_phase line 72
  14. lemma OAI.PlanarEndpoint.continuous_phase line 76
  15. lemma OAI.PlanarEndpoint.continuous_phase_parameters line 80
  16. lemma OAI.PlanarEndpoint.memLp_gaussian line 85
  17. lemma OAI.PlanarEndpoint.abel_integrable line 102
  18. def OAI.PlanarEndpoint.evolution line 119
  19. lemma OAI.PlanarEndpoint.evolution_integrable line 122
  20. lemma OAI.PlanarEndpoint.continuous_evolution line 129
  21. def OAI.PlanarEndpoint.gaussianWeight line 148
  22. lemma OAI.PlanarEndpoint.gaussianWeight_pos line 150
  23. lemma OAI.PlanarEndpoint.gaussianWeight_le_one line 152
  24. lemma OAI.PlanarEndpoint.abel_eq_weighted line 157
  25. lemma OAI.PlanarEndpoint.gaussian_error_integrable line 167
  26. lemma OAI.PlanarEndpoint.gaussian_error_tendsto_zero line 179
  27. lemma OAI.PlanarEndpoint.weighted_evolution_integrable line 200
  28. lemma OAI.PlanarEndpoint.norm_abel_sub_evolution_le line 213
  29. lemma OAI.PlanarEndpoint.abel_tendstoUniformly line 238
  30. def OAI.PlanarEndpoint.AnnularFourierSupport line 251
  31. lemma OAI.PlanarEndpoint.fourier_integrable_of_bounded_support line 254
  32. lemma OAI.PlanarEndpoint.AnnularFourierSupport.integrable line 264
  33. def OAI.PlanarEndpoint.shortTimeLevel line 272
  34. lemma OAI.PlanarEndpoint.isOpen_timeLevel line 275
  35. lemma OAI.PlanarEndpoint.measurableSet_shortTimeLevel line 289
  36. def OAI.PlanarEndpoint.ShortTimeWeakEstimate line 293
  37. lemma OAI.PlanarEndpoint.fourier_energy line 301
  38. lemma OAI.PlanarEndpoint.norm_evolution_le_fourierL1 line 316
  39. lemma OAI.PlanarEndpoint.fourierL1_le_support_energy line 324
  40. lemma OAI.PlanarEndpoint.sobolevWeight_one_le line 358
  41. lemma OAI.PlanarEndpoint.sobolev_energy_nonneg line 361
  42. lemma OAI.PlanarEndpoint.norm_le_hThirdNorm line 367
  43. lemma OAI.PlanarEndpoint.norm_evolution_le_bounded_frequency line 381
  44. lemma OAI.PlanarEndpoint.norm_evolution_le_low_frequency line 398
  45. lemma OAI.PlanarEndpoint.fourier_schwartz_ae line 408
  46. lemma OAI.PlanarEndpoint.fourier_schwartz_integrable line 419
  47. lemma OAI.PlanarEndpoint.phase_zero_eq_scaled_inverse_character line 424
  48. lemma OAI.PlanarEndpoint.evolution_schwartz_zero line 433
  49. lemma OAI.PlanarEndpoint.closedBall_ae_eq_ball line 453
  50. lemma OAI.PlanarEndpoint.diskAverage_eq_average line 459
  51. lemma OAI.PlanarEndpoint.diskNormAverage_eq_average line 467
  52. lemma OAI.PlanarEndpoint.ae_isLebesguePoint line 477
  53. lemma OAI.PlanarEndpoint.ae_diskAverage_tendsto line 489
  54. lemma OAI.PlanarEndpoint.lebesgueRepresentative_ae line 501
  55. def OAI.PlanarEndpoint.sobolevWeight line 509
  56. def OAI.PlanarEndpoint.sobolevMeasure line 510
  57. lemma OAI.PlanarEndpoint.continuous_sobolevWeight line 512
  58. lemma OAI.PlanarEndpoint.sobolevWeight_pos line 516
  59. instance OAI.PlanarEndpoint.sobolevMeasure_locallyFinite line 519
  60. lemma OAI.PlanarEndpoint.integrable_sq_sobolevMeasure_iff line 522
  61. lemma OAI.PlanarEndpoint.integral_sq_sobolevMeasure line 530
  62. lemma OAI.PlanarEndpoint.fourier_memLp_sobolev line 538
  63. lemma OAI.PlanarEndpoint.fourier_sub_ae line 545
  64. lemma OAI.PlanarEndpoint.hThirdNorm_eq_weighted_eLpNorm line 552
  65. lemma OAI.PlanarEndpoint.exists_smooth_compact_fourier_approx line 565
  66. lemma OAI.PlanarEndpoint.inHThird_of_fourier_memLp_sobolev line 577
  67. def OAI.PlanarEndpoint.frequencyDilation line 582
  68. lemma OAI.PlanarEndpoint.frequencyDilation_apply line 586
  69. def OAI.PlanarEndpoint.inverseCompactFourier line 589
  70. lemma OAI.PlanarEndpoint.fourier_inverseCompactFourier_ae line 594
  71. lemma OAI.PlanarEndpoint.exists_schwartz_hThird_approx line 604
  72. lemma OAI.PlanarEndpoint.gaussian_fourier_norm_integrable line 641
  73. lemma OAI.PlanarEndpoint.continuousAt_abel_parameters line 649
  74. lemma OAI.PlanarEndpoint.continuousOn_abel_parameters line 683
  75. def OAI.PlanarEndpoint.evolutionMultiplier line 692
  76. lemma OAI.PlanarEndpoint.norm_evolutionMultiplier line 695
  77. lemma OAI.PlanarEndpoint.continuous_evolutionMultiplier line 698
  78. lemma OAI.PlanarEndpoint.memLp_evolutionFourier line 702
  79. def OAI.PlanarEndpoint.l2Evolution line 710
  80. lemma OAI.PlanarEndpoint.l2Evolution_fourier_ae line 715
  81. lemma OAI.PlanarEndpoint.fourier_l2Evolution_ae line 721
  82. lemma OAI.PlanarEndpoint.norm_l2Evolution line 730
  83. lemma OAI.PlanarEndpoint.l2Evolution_zero line 742
  84. lemma OAI.PlanarEndpoint.l2Evolution_sub line 748
  85. lemma OAI.PlanarEndpoint.dist_l2Evolution line 765
  86. lemma OAI.PlanarEndpoint.inHThird_l2Evolution line 769
  87. lemma OAI.PlanarEndpoint.hThirdNorm_l2Evolution line 775
  88. lemma OAI.PlanarEndpoint.inverse_fourier_continuous line 789
  89. lemma OAI.PlanarEndpoint.inverse_fourier_pairing line 794
  90. lemma OAI.PlanarEndpoint.l2_inverse_fourier_ae line 806
  91. lemma OAI.PlanarEndpoint.integrable_mathlib_fourier line 845
  92. lemma OAI.PlanarEndpoint.integrable_evolutionFourier line 851
  93. lemma OAI.PlanarEndpoint.evolution_eq_mathlib_inverse line 859
  94. lemma OAI.PlanarEndpoint.l2Evolution_ae_evolution line 888
  95. abbrev OAI.PlanarEndpoint.Time line 899
  96. abbrev OAI.PlanarEndpoint.TimePath line 900
  97. lemma OAI.PlanarEndpoint.continuous_evolution_time line 902
  98. def OAI.PlanarEndpoint.evolutionPath line 909
  99. lemma OAI.PlanarEndpoint.continuous_evolutionPath line 912
  100. lemma OAI.PlanarEndpoint.mainConclusion_of_fourier_integrable line 924