OAI/MeasureTheory/Falconer/Estimates/ScalarNonporousFraction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Applying the binary sumset construction to obtain a positive fraction of actual porous levels in the regularized scalar tree.

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