OAI/Analysis/RieszRectifiability/Flatness/NeighborCellPlaneDirections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Direction comparison for neighboring cell planes

Bilateral plane estimates on nearby cells of comparable radii yield common support tubes. These tubes bound the normal projections between the two plane directions.

  1. theorem OAI.RieszRectifiability.neighbor_cell_plane_common_tubes line 21
  2. theorem OAI.RieszRectifiability.neighbor_cell_plane_directions_close line 67