OAI/Analysis/PlanarEndpoint/TimeSeparation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. lemma OAI.PlanarEndpoint.card_integer_neighbors line 17
  2. lemma OAI.PlanarEndpoint.separated_interval_points line 36
  3. lemma OAI.PlanarEndpoint.scaled_cutoff_memLp line 49
  4. abbrev OAI.PlanarEndpoint.DyadicGraph.Node line 57
  5. def OAI.PlanarEndpoint.DyadicGraph.nodeIndex line 59
  6. lemma OAI.PlanarEndpoint.DyadicGraph.nodeIndex_injective line 61
  7. lemma OAI.PlanarEndpoint.DyadicGraph.width_node line 70
  8. lemma OAI.PlanarEndpoint.DyadicGraph.interval_node line 73
  9. lemma OAI.PlanarEndpoint.DyadicGraph.node_interval_separation line 79
  10. lemma OAI.PlanarEndpoint.time_kernel_bound line 91
  11. lemma OAI.PlanarEndpoint.time_separation_uniform line 107