OAI/MeasureTheory/Falconer/Estimates/RotatedWeightedInverse.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The cell-scaled inverse in a fixed orthogonal angular frame

Only the angular variable changes. All spatial displacements, distance powers, frequencies and endpoint laws in the separated formula are the original ones.

  1. def OAI.Falconer.rotatedScaledWeightedInverseSum line 16
  2. def OAI.Falconer.rotatedScaledInverseTerm line 21
  3. theorem OAI.Falconer.rotatedScaledWeightedInverseSum_eq_terms line 30
  4. theorem OAI.Falconer.exists_rotated_scaled_weighted_inverse_order line 48