OAI/Analysis/LipschitzHilbert/Packets/ScaledPlanarPacket.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

General planar Schwartz profiles in the physical packet coordinates. The affine restriction retains Schwartz regularity and the carrier is removed exactly by vertical covariant differentiation.

  1. theorem OAI.LipschitzHilbert.affineRescale_antilipschitz line 13
  2. def OAI.LipschitzHilbert.scaledPlanarSlice line 23
  3. theorem OAI.LipschitzHilbert.scaledPlanarSlice_apply line 29
  4. theorem OAI.LipschitzHilbert.planarCarrier_temperate line 33
  5. def OAI.LipschitzHilbert.modulatedPlanarSlice line 38
  6. theorem OAI.LipschitzHilbert.modulatedPlanarSlice_apply line 44
  7. theorem OAI.LipschitzHilbert.modulatedPlanarSlice_norm line 56
  8. theorem OAI.LipschitzHilbert.modulatedPlanarSlice_vertical_hasDerivAt line 65
  9. theorem OAI.LipschitzHilbert.modulatedPlanarSlice_covariant line 88