OAI/MeasureTheory/Falconer/Estimates/ScalarNonporousDoubling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The nonporous alternative contradicts a small doubling bound once the explicit branching count exceeds the fixed-fold Pluennecke budget.

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