OAI/Analysis/RieszRectifiability/Surfaces/CoherentCellCharts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lipschitz charts from coherent cell fits

For each pair of points, a descendant at the separation scale supplies a nearby affine plane with small angle to a fixed subspace. The resulting lower bound on projected distances gives an inverse Lipschitz estimate and a ball parameterization of the piece.

  1. theorem OAI.RieszRectifiability.projection_separates_of_coherent_cell_fits line 22
  2. theorem OAI.RieszRectifiability.exists_ball_lipschitz_cover_of_coherent_cell_fits line 50