OAI/MeasureTheory/Falconer/Fourier/SafeStationaryChart.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A global smooth extension of the fixed local stationary chart

The extension equals the actual chart near every direction in the support of the fixed patch mask. It exists only to express its finite derivatives as globally smooth separated factors; the stationary coefficients remain the original coefficients.

  1. def OAI.Falconer.stationaryExtensionBump line 17
  2. def OAI.Falconer.stationarySafePoint line 23
  3. theorem OAI.Falconer.stationarySafePoint_contDiff line 26
  4. theorem OAI.Falconer.stationarySafePoint_near line 31
  5. theorem OAI.Falconer.stationarySafePoint_bound line 38
  6. theorem OAI.Falconer.stationarySafePoint_nonantipodal line 53
  7. def OAI.Falconer.safeStationaryChart line 66
  8. theorem OAI.Falconer.safeStationaryChart_contDiff line 72
  9. theorem OAI.Falconer.safeStationaryChart_zero line 89
  10. def OAI.Falconer.safeStationaryDensity line 100
  11. theorem OAI.Falconer.safeStationaryDensity_contDiff line 103
  12. theorem OAI.Falconer.maskedStationaryCoefficient_safe line 114