OAI/Analysis/RieszRectifiability/Projections/ChartProjectionResidual.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Projection bounds for chart residuals

A Lipschitz bound on the displacement residual controls the tangential coordinate error of a perturbed chart. The normal component inherits the sum of this bound and the original normal Lipschitz constant, by contractivity of orthogonal projection.

  1. theorem OAI.RieszRectifiability.projected_chart_error_lipschitz_of_residual line 21
  2. theorem OAI.RieszRectifiability.normal_chart_lipschitz_of_residual line 44