OAI/Analysis/RieszRectifiability/Flatness/NormalHyperplaneTangent.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Tangent measures supported on a normal hyperplane

Half-space support is preserved by centered blowups. Decay of positive normal moments forces the limiting support onto the boundary hyperplane; growth compactness then produces a nonzero tangent measure with this constraint and two-sided growth bounds.

  1. theorem OAI.RieszRectifiability.blowup_support_in_halfspace line 23
  2. theorem OAI.RieszRectifiability.blowup_limit_support_in_normal_hyperplane line 34
  3. theorem OAI.RieszRectifiability.exists_nonzero_normal_hyperplane_tangent line 71