OAI/MeasureTheory/Falconer/Estimates/ScaledWeightedInverse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The inverse expansion at the actual cell scale

Only the distance weight is rescaled. The oscillatory phase still uses the original displacement and original radial frequency. The integer inverse powers therefore match the spatial Fourier separation at the cell scale.

  1. def OAI.Falconer.scaledWeightedInverseSum line 16
  2. theorem OAI.Falconer.scaled_weighted_inverse_coefficient line 24
  3. theorem OAI.Falconer.scaledWeightedInverseSum_eq line 34
  4. theorem OAI.Falconer.scaled_weighted_inverse_distance line 45
  5. theorem OAI.Falconer.exists_scaled_weighted_inverse_order line 50