OAI/MeasureTheory/Falconer/Fourier/StationaryWeightCancellation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact cancellation of the original distance weight

The fixed weight q^(-(d-1)/2) cancels the base spatial power in the inverse expansion. Only the integer inverse powers need spatial Fourier separation. The same weight occurs in each direct factor.

  1. theorem OAI.Falconer.stationary_weighted_inverse_power line 15
  2. theorem OAI.Falconer.stationary_direct_power line 27
  3. theorem OAI.Falconer.stationary_direct_pair_power line 34