OAI/MeasureTheory/Falconer/Fourier/PositiveFourier.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Fourier control of the actual positive collision state

The tolerance is the manuscript's 100(d+1)2⁻ᵗ. The frequency interval is enlarged from 2ᵗ/(d+1) to 2ᵗ using positivity, with a fixed dimensional constant. No regularity of the tested pair measure is required here.

  1. theorem OAI.Falconer.charFun_testedCellDistance line 17
  2. theorem OAI.Falconer.dyadic_distance_collision_fourier line 24
  3. theorem OAI.Falconer.positiveCollisionCount_fourier line 68