OAI/MeasureTheory/Falconer/Estimates/ScalarNonporousGrowth.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual nonporous blocks, including skipped levels, produce a large separated subset of a fixed-fold sumset of the original leaf centers.

  1. theorem OAI.Falconer.Regularization.scalar_nonporous_growth line 10