OAI/Analysis/RieszRectifiability/Foundations/GrowthVolumeDomination.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Volume domination from intrinsic upper growth

An upper growth bound in the intrinsic Euclidean dimension implies domination by Lebesgue measure. The density bound is normalized by the unit-ball volume and includes the dimensional factor needed for closed-ball comparison.

  1. def OAI.RieszRectifiability.intrinsicGrowthDensityBound line 22
  2. theorem OAI.RieszRectifiability.intrinsic_growth_le_volume line 25
  3. theorem OAI.RieszRectifiability.intrinsic_growth_absolutelyContinuous line 60