OAI/MeasureTheory/Falconer/Graphs/BipartitePivot.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The dense-neighborhood pivot used in the scalar additive-energy argument. Integer vertices are sufficient for the quantized sumsets.

  1. def OAI.Falconer.integerNeighbors line 10
  2. def OAI.Falconer.integerCommonNeighbors line 13
  3. def OAI.Falconer.integerBadPairs line 16
  4. def OAI.Falconer.integerBadPairsAt line 19
  5. theorem OAI.Falconer.integer_bad_pairs_sum line 23
  6. theorem OAI.Falconer.integer_bad_pairs_sum_le line 30
  7. theorem OAI.Falconer.integer_dense_pivot line 43