OAI/Analysis/RieszRectifiability/Nets/OriginalADCellBadCountBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bad-cell count budgets inside a support cell

Removing a multiplicity tail leaves a measurable set with uniformly bounded bad-cell counts relative to every descendant. A zero count forbids all bad descendants containing the point, and hence places that point in the corresponding good-region limit.

  1. theorem OAI.RieszRectifiability.original_AD_Riesz_cell_bad_count_budget line 22
  2. theorem OAI.RieszRectifiability.zero_bad_count_mem_relative_region_limit line 61