OAI/Analysis/RieszRectifiability/Surfaces/OriginalADMatchedSurfaceModels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Matched surface models for an AD-regular measure

Uniform-precision area models combine with the native surface geometry to give matched projection coverage at every scale. The top-mass and AD constants are chosen before the precision and support cell, while the resulting surface keeps its exact support, infinite support diameter, and two-sided growth bounds.

  1. theorem OAI.RieszRectifiability.exists_original_AD_matched_surface_models line 24