OAI/MeasureTheory/Falconer/Fourier/CoordinateIntegral.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Isolating one Euclidean chart coordinate

This change of coordinates preserves the actual Euclidean volume. It therefore allows the scalar nonstationary bound to be integrated in the remaining chart coordinates without any additional measure assumption.

  1. def OAI.Falconer.coordinateEquiv line 17
  2. def OAI.Falconer.coordinateJoin line 23
  3. theorem OAI.Falconer.coordinateJoin_eq line 26
  4. theorem OAI.Falconer.coordinateEquiv_measurePreserving line 33
  5. theorem OAI.Falconer.coordinate_integral line 45
  6. theorem OAI.Falconer.coordinate_iterated_integral line 51