OAI/MeasureTheory/Falconer/Estimates/RotatedNonstationary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform rotation of the spherical nonstationary estimate

The same constant applies to every cap center and every choice of its first tangent direction. The displacement is pulled back by the linear isometry, while the amplitude keeps its original point labels.

  1. def OAI.Falconer.rotatedChartAmplitude line 18
  2. theorem OAI.Falconer.rotated_sphere_chart_nonstationary line 22