OAI/Analysis/RieszRectifiability/Foundations/VitaliLocalMassCharge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A disjoint Vitali selection converts local charges on fivefold enlarged balls into a comparison between the total mass of a set and the mass of its containing region.

  1. theorem OAI.RieszRectifiability.measure_le_of_local_fivefold_charges line 18