OAI/MeasureTheory/Falconer/Shells/RegularClassShell.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform shell estimate for the original regularized class laws

The parameters are chosen before the scale and the classes. A single entry index for each class pair works for every measurable product restriction.

  1. theorem OAI.Falconer.exists_regular_class_shell line 17