OAI/MeasureTheory/Falconer/Estimates/PathDifferenceBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Counting four-edge paths with a common difference. This proves the small-difference-set conclusion needed by the additive-energy argument.

  1. theorem OAI.Falconer.four_path_difference_bound line 12
  2. theorem OAI.Falconer.integer_dense_small_difference line 63