OAI/Analysis/PlanarEndpoint/GraphLocalization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. lemma OAI.PlanarEndpoint.scaled_cutoff_annular line 19
  2. lemma OAI.PlanarEndpoint.real_univ_finsetSum line 34
  3. lemma OAI.PlanarEndpoint.graphLp_congr_measure line 40
  4. lemma OAI.PlanarEndpoint.graph_spatial_bound_of_shortTime line 48