OAI/Analysis/RieszRectifiability/Surfaces/SurfaceBallCellCover.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite cell centers near a surface ball

Compactness makes the separated lattice centers near a ball finite. A Euclidean packing estimate bounds their number uniformly in the ball center and radius.

  1. theorem OAI.RieszRectifiability.surface_ball_cell_centers_finite line 20
  2. def OAI.RieszRectifiability.surfaceBallCellCenters line 32
  3. theorem OAI.RieszRectifiability.mem_surfaceBallCellCenters line 36
  4. theorem OAI.RieszRectifiability.surfaceBallCellCenters_card_le line 41
  5. theorem OAI.RieszRectifiability.surface_ball_covered_by_selected_cells_off_exceptional line 72
  6. theorem OAI.RieszRectifiability.selected_surface_ball_cell_subset_seven_ball line 85