OAI/MeasureTheory/Falconer/Estimates/ScalarBinaryGeometric.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Geometrically spaced nonporous binary increments force growth of a fixed-fold sumset, and hence contradict an appropriately small sumset.

  1. theorem OAI.Falconer.scalar_scaled_binary_growth line 11
  2. theorem OAI.Falconer.scalar_geometric_binary_growth line 50
  3. theorem OAI.Falconer.scalar_geometric_binary_cells line 69
  4. theorem OAI.Falconer.scalar_geometric_binary_doubling_bound line 83