OAI/Analysis/RieszRectifiability/Surfaces/NativeSurfaceArea.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic surface-area measures

The native surface-area measure is Hausdorff measure restricted to the surface. Upper area growth gives local finiteness and regularity, while lower area bounds identify the support when the surface is closed.

  1. def OAI.RieszRectifiability.nativeSurfaceArea line 21
  2. theorem OAI.RieszRectifiability.nativeSurfaceArea_apply line 24
  3. theorem OAI.RieszRectifiability.nativeSurfaceArea_open_ball_lower line 29
  4. theorem OAI.RieszRectifiability.nativeSurfaceArea_global_upper_growth line 48
  5. theorem OAI.RieszRectifiability.nativeSurfaceArea_regular line 62
  6. theorem OAI.RieszRectifiability.nativeSurfaceArea_support line 74