OAI/MeasureTheory/Falconer/Geometry/ScalarRuzsaCovering.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ruzsa covering at a fixed scalar resolution, with actual centers from the original set and an explicit rounding error.

  1. theorem OAI.Falconer.scalar_ruzsa_covering line 11