OAI/Analysis/RieszRectifiability/Nets/CountableCellMultiplicity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Countable cell multiplicity

The sum of cell indicators measures pointwise overlap. Its integral is the total cell mass, giving tail bounds, almost-everywhere finite incidence, and lower bounds for the mass where the multiplicity is controlled.

  1. def OAI.RieszRectifiability.cellMultiplicity line 20
  2. theorem OAI.RieszRectifiability.cellMultiplicity_measurable line 23
  3. theorem OAI.RieszRectifiability.lintegral_cellMultiplicity line 28
  4. theorem OAI.RieszRectifiability.cellMultiplicity_tail_bound line 36
  5. theorem OAI.RieszRectifiability.ae_finite_cell_incidence line 45
  6. theorem OAI.RieszRectifiability.cellMultiplicity_good_mass_lower line 60
  7. theorem OAI.RieszRectifiability.cellMultiplicity_half_mass line 70