OAI/Analysis/LipschitzHilbert/Fourier/PlanarSchwartzDecay.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed product-envelope bounds for general planar Schwartz packets. The constants are obtained from their actual weighted seminorms.

  1. def OAI.LipschitzHilbert.planarPolynomialWeight line 12
  2. theorem OAI.LipschitzHilbert.planarPolynomialWeight_pos line 15
  3. theorem OAI.LipschitzHilbert.planarPolynomialWeight_temperate line 18
  4. def OAI.LipschitzHilbert.planarEnvelopeConstant line 27
  5. theorem OAI.LipschitzHilbert.planarEnvelopeConstant_pos line 31
  6. theorem OAI.LipschitzHilbert.planar_schwartz_envelope line 34
  7. theorem OAI.LipschitzHilbert.planar_covariant_jet_envelope line 50