OAI/MeasureTheory/Falconer/Measures/ScalarProductInterpolation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Interpolating the fine packing bound with scalar nonconcentration gives a higher-dimensional ball exponent for the actual product set.

  1. theorem OAI.Falconer.nonnegative_bound_interpolation line 9
  2. theorem OAI.Falconer.scalarProductPoints_interpolated_ball line 23
  3. theorem OAI.Falconer.scalar_product_profile_factor line 42