OAI/Analysis/RieszRectifiability/Nets/CapturedCellSeedMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Depth gaps between captured cells are charged to intervening cells. The resulting pointwise seed-multiplicity bound integrates to a mass estimate for the finite captured family.

  1. theorem OAI.RieszRectifiability.captured_cell_seed_mass_bound line 20