OAI/MeasureTheory/Falconer/Estimates/ScalarClusterSums.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Disjoint scalar projection cells outside the explicitly bounded exceptional coefficient set. The children are the actual original finite clusters, so their covering numbers can be iterated.

  1. theorem OAI.Falconer.scalar_cells_disjoint_of_centers line 13
  2. theorem OAI.Falconer.scalar_cluster_sum_near line 33
  3. theorem OAI.Falconer.scalar_cluster_sums_cells line 47