OAI/Analysis/RieszRectifiability/Uniformity/Rectifiability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative ball images with constants chosen before the measure

Clean-cell charts with relative deficit ζ yield genuine ball images with mass fraction (1 - ζ) / (C * 32 ^ n) and the rescaled Lipschitz bound. The final assembly chooses the surface-piece and restart budgets from the fixed dimension, AD constant, and common Riesz bound before introducing the measure. Degenerate supports are handled directly through the admissible-radius condition.

  1. theorem OAI.RieszRectifiability.quantitative_ball_images_of_clean_cell_deficits line 24
  2. theorem OAI.RieszRectifiability.quantitative_higher_codimension_riesz_rectifiability line 89

    Distinct definitions of this name: ComparatorChallenges/RieszQuantitative.lean:57 (same statement text; different proof or body). Qualify references as OAI.RieszRectifiability.quantitative_higher_codimension_riesz_rectifiability@path.