OAI/Analysis/RieszRectifiability/Foundations/AnnularBoundedTangents.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Tangents with global smooth annular bounds

The global smooth annular bound is stable under blowups and compact-test limits. This stability preserves the bound when extracting a nonzero tangent supported on a proper hyperplane, so that the dimension-reduction argument can be iterated.

  1. def OAI.RieszRectifiability.GlobalSmoothAnnularBound line 22
  2. theorem OAI.RieszRectifiability.GlobalSmoothAnnularBound.blowup line 26
  3. theorem OAI.RieszRectifiability.GlobalSmoothAnnularBound.compact_limit line 34
  4. theorem OAI.RieszRectifiability.GlobalSmoothAnnularBound.of_local_tangent line 46
  5. theorem OAI.RieszRectifiability.exists_annular_bounded_hyperplane_tangent line 58