OAI/MeasureTheory/Falconer/Estimates/UniformDescriptorFactors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One separated factor family for all scales and regularized classes

The countable label includes the scale and class before the operator is constructed. Thus the constants in HasOrder are selected for this whole family, not separately at each scale.

  1. theorem OAI.Falconer.uniform_descriptor_inverse_factors line 17