OAI/MeasureTheory/Falconer/Estimates/InterpolatedTubeKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Interpolation of the regularity and separation bounds on a common pencil. The intermediate potential exponent stays strictly below the point dimension, so only the already proved finite geometric-series bound is used.

  1. theorem OAI.Falconer.interpolate_two_power_bounds line 12
  2. theorem OAI.Falconer.intersect_tube_interpolated_bound line 36