OAI/MeasureTheory/Falconer/Geometry/CommonSmallProjections.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common regular parameters with large subsets having small projections. This is the exact finite configuration produced before the projection theorem in Orponen--Shmerkin, Appendix A.7. No projection estimate is assumed here.

  1. theorem OAI.Falconer.common_regular_small_projections line 11