OAI/Analysis/LipschitzHilbert/Fourier/PlanarSchwartzInversion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Fourier inversion on the actual product plane, and the frozen multiplier identity for every planar Schwartz input.

  1. def OAI.LipschitzHilbert.planarFourierSchwartz line 14

    Source documentation

    The planar transform remains Schwartz, with the product norm.

    def planarFourierSchwartz (f : SchwartzMap (ℝ×ℝ) ℂ) : SchwartzMap (ℝ×ℝ) ℂ :=
…
  2. theorem OAI.LipschitzHilbert.planarFourierSchwartz_apply line 18
  3. theorem OAI.LipschitzHilbert.planarFourier_integrable line 22
  4. theorem OAI.LipschitzHilbert.planarFourier_inversion line 28
  5. theorem OAI.LipschitzHilbert.schwartz_frozen_slope_multiplier line 38