OAI/Analysis/RieszRectifiability/Flatness/LocalAnnularFlatBall.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local flat balls from annular bounds

Local smooth annular control and capped lower growth force arbitrarily small balls with small bilateral beta number. Otherwise a tangent inherits global nonflatness and annular control, contradicting termination of the supporting-plane dimension drop.

  1. theorem OAI.RieszRectifiability.exists_local_flat_ball_of_annular_bound line 21