OAI/Analysis/LipschitzHilbert/Fourier/PlanarCovariantJet.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The first two covariant vertical derivatives of a general planar Schwartz packet, restricted to a reference line.

  1. def OAI.LipschitzHilbert.planarVerticalDerivative line 11
  2. theorem OAI.LipschitzHilbert.planarVerticalDerivative_apply line 14
  3. def OAI.LipschitzHilbert.planarCovariantDerivative line 17
  4. theorem OAI.LipschitzHilbert.planarCovariantDerivative_slice line 21
  5. def OAI.LipschitzHilbert.planarCovariantJet line 30
  6. theorem OAI.LipschitzHilbert.planarCovariantJet_slice_zero line 35
  7. theorem OAI.LipschitzHilbert.planarCovariantJet_slice_one line 43
  8. theorem OAI.LipschitzHilbert.planarCovariantJet_slice_continuous line 52
  9. theorem OAI.LipschitzHilbert.planarCovariantJet_slice_differentiable line 57