OAI/Analysis/RieszRectifiability/Surfaces/RieszFromUniformSurfacePieces.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform rectifiability from restart surface pieces

HasUniformRestartSurfacePieces uniformly bounds the number and Lipschitz constants of pieces covering restart models up to a prescribed weighted area loss. Combining this data with AD regularity and the Riesz bound gives clean-cell charts with half-mass deficit, and hence uniform rectifiability.

  1. def OAI.RieszRectifiability.HasUniformRestartSurfacePieces line 22
  2. theorem OAI.RieszRectifiability.uniformlyRectifiable_of_Riesz_and_uniform_restart_surface_pieces line 37