OAI/MeasureTheory/Falconer/Fourier/ChartBumps.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Cap bump derivatives in every rotated spherical chart

The constants depend only on the ambient dimension and derivative order. The cap center, rotation, radius and transverse chart coordinate remain free.

  1. def OAI.Falconer.rotatedChartCurve line 17
  2. theorem OAI.Falconer.rotatedChartCurve_contDiff line 21
  3. theorem OAI.Falconer.rotatedChartCurve_norm line 34
  4. theorem OAI.Falconer.capBump_rotated_derivatives line 39
  5. theorem OAI.Falconer.capBump_rotated_derivative_zero line 66