OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFourierProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact Fourier product formula on the physical Schwartz domain

The previously constructed physical multiplication and frequency convolution give the radian Fourier product formula, including its normalization.

  1. theorem OAI.DefocusingNLS.homogeneousFrequencyEmbedding_injective line 18
  2. theorem OAI.DefocusingNLS.radianFourierKernel_schwartzProduct line 26
  3. theorem OAI.DefocusingNLS.radianFourierKernel_schwartzProduct_apply line 43
  4. theorem OAI.DefocusingNLS.schwartz_mul_sub_integrable line 51