OAI/MeasureTheory/Falconer/Radial/PublishedHeavyPlates.lean

The published heavy-hyperplane cover used by the coarse-filter construction

P. Shmerkin, A non-linear version of Bourgain's projection theorem, J. Eur. Math. Soc. 25 (2023), 4155--4204, Appendix B, Lemma B.3, printed pages 4201--4202, DOI 10.4171/JEMS/1283. Publisher PDF: https://ems.press/content/serial-article-files/32954 .

This is only the hyperplane case k=d-1, at the single scale used in the application, with heavy threshold delta^(a/8192). The lower-dimensional concentration hypothesis is retained explicitly. The conclusion covers each heavy plate in the unit ball by one of finitely many thicker plates. The constant is allowed to depend on the dimension, a and C. No assertion about dyadic filters, retained product mass or distance sets is assumed.