OAI/Analysis/PlanarEndpoint/AnnularCutoff.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. def OAI.PlanarEndpoint.outerBump line 14
  2. def OAI.PlanarEndpoint.innerBump line 15
  3. def OAI.PlanarEndpoint.annularCutoff line 16
  4. lemma OAI.PlanarEndpoint.annularCutoff_smooth line 18
  5. lemma OAI.PlanarEndpoint.annularCutoff_zero_small line 21
  6. lemma OAI.PlanarEndpoint.annularCutoff_zero_large line 27
  7. lemma OAI.PlanarEndpoint.annularCutoff_support line 33
  8. lemma OAI.PlanarEndpoint.annularCutoff_compact line 42
  9. lemma OAI.PlanarEndpoint.annularCutoff_bound line 47
  10. lemma OAI.PlanarEndpoint.annularCutoff_one line 52
  11. lemma OAI.PlanarEndpoint.dyadic_annular_cover line 57
  12. lemma OAI.PlanarEndpoint.scaled_annularCutoff_one line 66
  13. lemma OAI.PlanarEndpoint.graph_square_sum_of_shortTime line 74