OAI/Analysis/PlanarEndpoint/SpatialGrid.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Gaussian regularization, Fourier evolution and endpoint maximal estimates.

  1. abbrev OAI.PlanarEndpoint.GridBox line 14
  2. def OAI.PlanarEndpoint.gridLabel line 16
  3. def OAI.PlanarEndpoint.gridCell line 19
  4. def OAI.PlanarEndpoint.gridCenter line 22
  5. lemma OAI.PlanarEndpoint.measurable_gridLabel line 25
  6. lemma OAI.PlanarEndpoint.measurableSet_gridCell line 32
  7. lemma OAI.PlanarEndpoint.gridCell_coord line 36
  8. lemma OAI.PlanarEndpoint.gridCell_in_ball line 50
  9. lemma OAI.PlanarEndpoint.gridLabel_mem_box line 65
  10. lemma OAI.PlanarEndpoint.gridCell_disjoint line 88
  11. lemma OAI.PlanarEndpoint.gridBox_injective line 94
  12. lemma OAI.PlanarEndpoint.grid_partition line 100
  13. lemma OAI.PlanarEndpoint.grid_restrict_eq_sum line 109
  14. def OAI.PlanarEndpoint.gridNear line 121
  15. lemma OAI.PlanarEndpoint.gridNear_symm line 124
  16. lemma OAI.PlanarEndpoint.gridNear_degree line 129
  17. lemma OAI.PlanarEndpoint.grid_far_distance line 144