OAI/MeasureTheory/Falconer/Estimates/UniformDescriptorFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common scale threshold for every inverse order used in the shell

The finite inverse family and all normalization constants are selected before any scale label. Taking the finite maximum of their thresholds keeps that quantifier order through the scalar shell application.

  1. theorem OAI.Falconer.normalized_descriptor_inverse_orders line 15