OAI/MeasureTheory/Falconer/Estimates/DescriptorInverseFactors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Measurable stationary factors for the actual descriptor product

The finite expansion is applied to the original spatially anchored masks. Every nonzero factor retains every old descriptor test at its own endpoint.

  1. theorem OAI.Falconer.descriptor_inverse_factors line 16