OAI/Analysis/PlanarEndpoint/GraphTree.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. instance OAI.PlanarEndpoint.volume_ball_isFiniteMeasure line 18
  2. lemma OAI.PlanarEndpoint.graph_node_energy_of_shortTime line 22
  3. def OAI.PlanarEndpoint.normalizedDyadicVector line 56
  4. lemma OAI.PlanarEndpoint.graph_tree_levels_of_shortTime line 63
  5. lemma OAI.PlanarEndpoint.norm_smul_sq_bound line 119
  6. lemma OAI.PlanarEndpoint.graph_root_sum_of_shortTime line 131