OAI/MeasureTheory/Falconer/Estimates/ScalarSignedRuzsa.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The other sign of the scalar Ruzsa triangle inequality, with the same rounding loss.

  1. theorem OAI.Falconer.sub_scalarCells_subset line 10
  2. theorem OAI.Falconer.sub_scalarCells_card line 24
  3. theorem OAI.Falconer.scalar_ruzsa_sum_triangle line 32