OAI/Analysis/RieszRectifiability/Nets/CellRegionMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mass decomposition for a cell region

The clean root cell splits into the region limit and the pairwise disjoint stopping cells. Countability of descendants and measurability of the cells turn this partition into an exact identity between the root mass, the limit mass, and the sum of stop masses.

  1. theorem OAI.RieszRectifiability.cellRegion_mass_identity line 21
  2. theorem OAI.RieszRectifiability.cellRegion_stopping_mass_le_top line 43