OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousPhysicalFourierJets.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cartesian jets of the actual physical representative

Up to order two, derivatives are ordinary inverse Fourier integrals. The restriction n ≤ 2 is exactly what k > 8 supplies in dimension twelve.

  1. theorem OAI.DefocusingNLS.physical_fourier_phase line 19
  2. theorem OAI.DefocusingNLS.physical_fourier_scalar line 24
  3. theorem OAI.DefocusingNLS.iteratedFDeriv_homogeneousPhysical line 29