OAI/MeasureTheory/Falconer/Geometry/SamplingGrid.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite planar query balls for simultaneous iid estimates

Rounding one point of a ball to the spatial mesh and rounding its radius up to an integer mesh multiple gives a query ball with radius at most eight times the original radius. The number of queries is polynomial in the reciprocal mesh. This is the finite-grid step in ang:sample-caps.

  1. def OAI.Falconer.planarMesh line 20
  2. def OAI.Falconer.planarGrid line 23
  3. theorem OAI.Falconer.planarGrid_card line 26
  4. theorem OAI.Falconer.planar_mesh_approximation line 32
  5. def OAI.Falconer.planarQueries line 68
  6. theorem OAI.Falconer.planarQueries_card line 71
  7. theorem OAI.Falconer.planar_ball_query line 75