OAI/Analysis/RieszRectifiability/Flatness/UniformNonflatTangents.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform bilateral nonflatness persists, with a fixed loss, under compact-test limits and blowups. Global lower growth supplies infinite support diameter for the limiting argument.

  1. theorem OAI.RieszRectifiability.GlobalBilateralLower.compact_limit_global line 19
  2. theorem OAI.RieszRectifiability.GlobalBilateralLower.tangent line 36