OAI/MeasureTheory/Falconer/Estimates/ScalarSubsetTransfer.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transferring a small projection from an overlapping subset to its reference set. Every denominator remains an actual covering number.

  1. theorem OAI.Falconer.scalarCells_mono line 10
  2. theorem OAI.Falconer.scalar_subset_sum_transfer line 13
  3. theorem OAI.Falconer.scalar_subset_difference_transfer line 40