OAI/Analysis/RieszRectifiability/Rigidity/FourierJetMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fourier jets and Schwartz moments

Iterated directional Fourier derivatives correspond to polynomially weighted Schwartz functions. Evaluating these derivatives at zero expresses Fourier jets as integrable moments with the appropriate Fourier normalization factor.

  1. def OAI.RieszRectifiability.fourierDerivativeFactor line 21
  2. def OAI.RieszRectifiability.fourierMomentSchwartz line 23
  3. theorem OAI.RieszRectifiability.fourierMomentSchwartz_apply line 29
  4. theorem OAI.RieszRectifiability.iteratedLineDeriv_fourier_moment line 45
  5. theorem OAI.RieszRectifiability.fourier_jet_at_zero_eq_moment line 54
  6. theorem OAI.RieszRectifiability.fourier_jet_moment_integrable line 62