OAI/MeasureTheory/Falconer/Estimates/PacketRepresentativeBand.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A weighted image can be thinned to representatives with comparable numbers of original witnesses, retaining both regularity and total mass.
- theorem
OAI.Falconer.packet_representative_bandline 11