OAI/Analysis/RieszRectifiability/Surfaces/ActualNativeSurfaceGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Geometry of the native area measure on a limit surface

Two-sided Hausdorff area bounds on a closed embedded active-region limit image give regularity, exact support, AD regularity, and infinite support diameter for its native area measure. Matched projection estimates then transfer to that support with the same explicit flatness and disk-coverage constants.

  1. theorem OAI.RieszRectifiability.active_region_native_surface_geometry line 23