OAI/MeasureTheory/Falconer/Estimates/ScalarIncrementSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Selecting nearly equal scalar increments among finitely many copies. This is the scalar pigeonhole step in the nonporous sumset construction.

  1. theorem OAI.Falconer.scalar_increment_selection line 10