OAI/Analysis/RieszRectifiability/Surfaces/NativeCoreAreaFraction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A uniform fraction for core area

The core-area fraction depends only on the dimension and upper growth constant. Its coefficient bound compares lattice-cell mass with the Hausdorff measure of a plane disk at the smaller core scale.

  1. def OAI.RieszRectifiability.nativeCoreAreaFraction line 23
  2. theorem OAI.RieszRectifiability.nativeCoreAreaFraction_pos_le_half line 27
  3. theorem OAI.RieszRectifiability.nativeCoreAreaFraction_coefficient_bound line 33
  4. theorem OAI.RieszRectifiability.native_core_disk_area_ge_double_fraction line 43