OAI/Analysis/RieszRectifiability/Surfaces/RegionRepresentativeCharts.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lipschitz charts for region representatives

Good cells at the scale of each pair provide affine-plane tube and angle bounds. These bounds make projection onto the reference plane separate region representatives with inverse Lipschitz constant two. A Lipschitz extension then covers the representatives by the image of a ball in the Euclidean space of the plane's dimension.

  1. theorem OAI.RieszRectifiability.projection_separates_region_representatives line 22
  2. theorem OAI.RieszRectifiability.exists_ball_lipschitz_cover_of_region_representatives line 57