OAI/Analysis/RieszRectifiability/Flatness/AdjacentCellPlaneDirections.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Comparing planes at adjacent cell scales

The factor of sixty-four between parent and child radii allows bilateral approximation to transfer plane tubes across adjacent cells. A local plane comparison then bounds the component of each child-plane direction orthogonal to the parent-plane direction.

  1. theorem OAI.RieszRectifiability.SupportCellDescendant.radius_parent_eq_64 line 21
  2. theorem OAI.RieszRectifiability.adjacent_cell_plane_tube_transfer line 29
  3. theorem OAI.RieszRectifiability.adjacent_cell_plane_direction_bound line 65