OAI/MeasureTheory/Falconer/Measures/ProductProjectionReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The geometric product configuration yields a single regular parameter set and many large subsets with small projections. This is the preparation for the strict projection gain in Orponen--Shmerkin, Proposition A.7.

  1. theorem OAI.Falconer.product_projection_reduction line 11