OAI/Analysis/RieszRectifiability/Surfaces/MatchedSurfaceBallDepthCharts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-depth charts on surface balls

Finite unions of matched-surface cell charts produce maps from Euclidean balls. The construction retains the finite-depth mass-deficit estimate and an explicit Lipschitz bound determined by the cell-chart bound and the covering multiplicity.

  1. theorem OAI.RieszRectifiability.exists_matched_surface_ball_depth_chart line 41