OAI/Analysis/PlanarEndpoint/Extension.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. def OAI.PlanarEndpoint.BoundedFourierSupport line 14
  2. lemma OAI.PlanarEndpoint.BoundedFourierSupport.integrable line 17
  3. lemma OAI.PlanarEndpoint.BoundedFourierSupport.sub line 22
  4. lemma OAI.PlanarEndpoint.inverseCompactFourier_boundedSupport line 32
  5. lemma OAI.PlanarEndpoint.inHThird_sub line 44
  6. lemma OAI.PlanarEndpoint.hThirdNorm_nonneg line 51
  7. lemma OAI.PlanarEndpoint.hThirdNorm_sub_le line 53
  8. lemma OAI.PlanarEndpoint.hThirdNorm_sub_comm line 69
  9. lemma OAI.PlanarEndpoint.evolution_sub line 76
  10. lemma OAI.PlanarEndpoint.evolutionPath_sub line 87
  11. lemma OAI.PlanarEndpoint.exists_schwartz_bounded_hThird_approx line 94
  12. lemma OAI.PlanarEndpoint.exists_fast_bounded_approximation line 127
  13. lemma OAI.PlanarEndpoint.exists_timePath_limit_of_summable line 158
  14. lemma OAI.PlanarEndpoint.ae_summable_path_increments line 165
  15. def OAI.PlanarEndpoint.pathLimit line 179
  16. lemma OAI.PlanarEndpoint.stronglyMeasurable_pathLimit line 182
  17. lemma OAI.PlanarEndpoint.ae_tendsto_pathLimit_of_local_summable line 186
  18. lemma OAI.PlanarEndpoint.isometry_l2Evolution line 195
  19. lemma OAI.PlanarEndpoint.pathLimit_ae_l2Evolution line 198