OAI/MeasureTheory/Falconer/Estimates/RotatedInverse.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transporting the inverse amplitude in the angular variable

The endpoint laws and their dyadic cells are not changed. Only the sphere integration variable and the directional derivatives of its amplitude rotate.

  1. theorem OAI.Falconer.sphereOscillation_isometry line 16
  2. def OAI.Falconer.rotatedInverseAmplitude line 27
  3. theorem OAI.Falconer.rotatedInverseAmplitude_contDiff line 31
  4. theorem OAI.Falconer.rotatedInverseAmplitude_scaled_budget line 36
  5. theorem OAI.Falconer.rotated_inverse_sphere_sum line 54
  6. theorem OAI.Falconer.rotated_sphere_inverse_expansion line 66