OAI/Analysis/RieszRectifiability/Flatness/CappedNonflatTangents.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded rescaled centers eventually remain in any open neighborhood of the blowup center. This transfers local capped nonflatness to a global bilateral lower bound for tangent limits.

  1. theorem OAI.RieszRectifiability.scaled_bounded_centers_eventually_mem_open line 19
  2. theorem OAI.RieszRectifiability.global_bilateral_lower_of_capped_tangent line 33