OAI/MeasureTheory/Falconer/Estimates/AllDimensionalParallelExceptional.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform exceptional mass of all-dimensional parallel tests

The numerical linear-subpower estimate is independent of dimension. The parallel tests use the original class centers and the original sphere law.

  1. theorem OAI.Falconer.Regularization.uniform_parallel_exceptional line 18