OAI/Analysis/RieszRectifiability/Flatness/FlatSeedExcess.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Support tubes and initial excess bounds

A support tube of width η around an affine n-plane bounds the normalized squared excess on a ball of radius R by G * (η / R) ^ 2 under global upper growth. A positive tube threshold therefore seeds the excess estimates on a finite dyadic horizon, with the same plane serving at every intermediate scale.

  1. theorem OAI.RieszRectifiability.squaredExcess_le_of_support_tube line 22
  2. theorem OAI.RieszRectifiability.exists_positive_tube_threshold line 54
  3. theorem OAI.RieszRectifiability.initial_excess_horizon_of_support_tube line 65