OAI/MeasureTheory/Falconer/Fourier/MaskedStationaryJets.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Smooth fixed-patch extensions of actual stationary jets

The mask is one on the prepared inner cap and vanishes near the antipodal singularity of the chosen frame. No global spherical differential operator is assumed.

  1. def OAI.Falconer.stationaryPatchMask line 17
  2. theorem OAI.Falconer.stationaryPatchMask_contDiff line 20
  3. theorem OAI.Falconer.stationaryPatchMask_one line 23
  4. theorem OAI.Falconer.stationary_patch_ne_antipode line 27
  5. theorem OAI.Falconer.stationaryPatchMask_support line 37
  6. def OAI.Falconer.maskedStationaryCoefficient line 42
  7. theorem OAI.Falconer.maskedStationaryCoefficient_contDiff line 46
  8. theorem OAI.Falconer.quadraticJetCoefficient_zero_amplitude line 60
  9. theorem OAI.Falconer.actualStationaryCoefficient_zero_amplitude line 66
  10. theorem OAI.Falconer.maskedStationaryCoefficient_eq line 76