OAI/MeasureTheory/Falconer/Measures/DenseNeighborPruning.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Removing the few vertices with many bad partners leaves many common good partners for every retained pair. This is the path-counting part of the additive-energy refinement.

  1. theorem OAI.Falconer.dense_neighbor_pruning line 11
  2. theorem OAI.Falconer.integer_bad_pair_rows line 56
  3. theorem OAI.Falconer.integer_dense_good_partners line 72