OAI/Analysis/RieszRectifiability/Restart/ActiveProjectionSurfaceBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Surface bounds for active-level projections

Height bounds control the displacement of the active-level projection map on a surface. Local comparison with a reference affine plane also bounds the distance of the projected image from that plane at the current lattice scale.

  1. theorem OAI.RieszRectifiability.activeLevelProjectionMap_surface_displacement line 26
  2. theorem OAI.RieszRectifiability.activeLevelProjectionMap_image_plane_height line 40