OAI/Analysis/RieszRectifiability/Flatness/ContractedAffinePatch.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Failure of a lower norm bound produces a contracted unit direction. Translating an affine patch into a linear tube then gives a mass estimate for its image under the contracting map.

  1. theorem OAI.RieszRectifiability.exists_contracted_unit_direction_of_not_lower line 18
  2. theorem OAI.RieszRectifiability.infDist_translated_affine_direction line 38
  3. theorem OAI.RieszRectifiability.translated_affine_patch_subset_tube line 51
  4. theorem OAI.RieszRectifiability.contracted_affine_patch_translated_real_measure_bound line 66