OAI/Analysis/LipschitzHilbert/Fourier/PlanarSchwartzSlice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual Schwartz restrictions to affine reference lines. This applies to general two-variable packets, with no tensor factorization.

  1. theorem OAI.LipschitzHilbert.affineLine_antilipschitz line 13
  2. theorem OAI.LipschitzHilbert.affineLine_temperate line 20
  3. def OAI.LipschitzHilbert.planarSchwartzSlice line 29
  4. theorem OAI.LipschitzHilbert.planarSchwartzSlice_apply line 33
  5. theorem OAI.LipschitzHilbert.planarSchwartzSlice_hasDerivAt line 36
  6. theorem OAI.LipschitzHilbert.planarSchwartzSlice_vertical_hasDerivAt line 44
  7. theorem OAI.LipschitzHilbert.planarSchwartzSlice_jointContinuous line 52