OAI/MeasureTheory/Falconer/Estimates/ScalarCoefficientClosure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite additive and multiplicative closure used in the scalar sum-product argument. Each stage has an explicit coefficient radius.

  1. def OAI.Falconer.scalarCoefficientClosure line 11
  2. def OAI.Falconer.scalarCoefficientRadius line 16
  3. theorem OAI.Falconer.scalarCoefficientRadius_pos line 20
  4. theorem OAI.Falconer.scalarCoefficientClosure_bound line 25