OAI/MeasureTheory/Falconer/Estimates/DescriptorExceptional.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exceptional-direction bounds for each actual level-zero descriptor

The angular measure is a restriction of the original opposite marginal; its cap constant is never divided by a class mass.

  1. theorem OAI.Falconer.Regularization.uniform_descriptor_exceptional line 20