OAI/MeasureTheory/Falconer/Measures/DensityCellCharge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Charging the full masses of hit children before the final density deletion

  1. theorem OAI.Falconer.density_hit_children_charge line 12