OAI/MeasureTheory/Falconer/Incidence/BlockPrefixRetention.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

After a second block regularization, a large retained class has mass in each occupied parent comparable to that of the original class.

  1. theorem OAI.Falconer.Regularization.blockClass_prefix_retention line 11