OAI/MeasureTheory/Falconer/Fourier/ParametricJets.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth dependence of the actual quadratic stationary jets

The derivatives are taken only in the tangent variable. Joint smoothness of an amplitude therefore gives smooth dependence of every fixed quadratic jet on its external parameters, including the evaluation direction.

  1. theorem OAI.Falconer.partialFDeriv_contDiffAt line 20
  2. theorem OAI.Falconer.partialLaplacian_contDiffAt line 28
  3. theorem OAI.Falconer.partialIteratedLaplacian_contDiffAt line 47
  4. theorem OAI.Falconer.quadraticJetCoefficient_contDiffAt line 58