OAI/MeasureTheory/Falconer/Estimates/ScalarEnergyRefinement.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transfer the integer additive-energy refinement to separated real sets, preserving the original points and the quantized difference bound.

  1. theorem OAI.Falconer.same_scalar_cell_dist_lt line 11
  2. theorem OAI.Falconer.scalarCells_injective line 24
  3. theorem OAI.Falconer.scalar_energy_refinement line 31