OAI/MeasureTheory/Falconer/Estimates/ScalarSwitchProgression.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The nonporous branching step: a fixed number of original summands produces an approximate arithmetic progression by switching selected coordinates. The coordinate ordering is retained for recursive use.

  1. theorem OAI.Falconer.scalar_increment_ordering line 13
  2. theorem OAI.Falconer.scalar_switch_progression_error line 38
  3. theorem OAI.Falconer.scalar_switch_progression_separated line 49
  4. theorem OAI.Falconer.scalar_switch_prefix_displacement line 62
  5. theorem OAI.Falconer.scalar_sumset_progression line 75