OAI/MeasureTheory/Falconer/Geometry/IntegerFourPaths.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Four-edge paths and their sum labels. Injectivity of the labels is the counting step converting dense neighborhoods into small difference sets.

  1. abbrev OAI.Falconer.IntegerPath line 10
  2. def OAI.Falconer.integerFourPaths line 12
  3. theorem OAI.Falconer.integerFourPaths_card line 16
  4. theorem OAI.Falconer.integerFourPaths_lower line 22
  5. def OAI.Falconer.integerPathSums line 37
  6. theorem OAI.Falconer.integerPathSums_alternating line 40
  7. theorem OAI.Falconer.integerPathSums_injective line 46
  8. theorem OAI.Falconer.integerPathSums_mem line 60