OAI/Analysis/RieszRectifiability/Surfaces/SurfaceBallChartAssembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Assembling surface ball charts

Finite cell charts combine into a ball chart whose uncovered surface mass is controlled by the sum of the cell deficits. Restriction to the surface identifies this deficit with the corresponding Hausdorff measure.

  1. theorem OAI.RieszRectifiability.exists_surface_ball_chart_of_cell_deficits line 23