OAI/Analysis/RieszRectifiability/Foundations/HoleTangentMeasure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Tangent measures at a nearest point to a hole

Uniform growth bounds yield a nonzero subsequential blowup limit with inherited two-sided growth. At a point nearest to a hole, the rescaled quadratic constraint converges to a half-space constraint on the tangent measure's support.

  1. theorem OAI.RieszRectifiability.exists_blowup_measure_limit line 23
  2. theorem OAI.RieszRectifiability.exists_nonzero_halfspace_tangent_of_hole line 42