OAI/Analysis/RieszRectifiability/Surfaces/MatchedSurfaceDepthCharts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Matched surface charts with controlled loss

For surfaces of infinite support diameter, contracting projection regions provide finite-depth charts with geometric mass loss. Choosing the depth from a positive loss tolerance gives one Lipschitz bound valid at every lattice scale and cell.

  1. theorem OAI.RieszRectifiability.exists_matched_surface_depth_chart line 41
  2. theorem OAI.RieszRectifiability.exists_matched_surface_uniform_small_loss_chart line 65