OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousLaplacianDomain.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Two extra Fourier orders put the physical Laplacian in Y

  1. theorem OAI.DefocusingNLS.homogeneousFourierWeight_laplacian line 14
  2. theorem OAI.DefocusingNLS.homogeneous_memLp_laplacian line 42
  3. theorem OAI.DefocusingNLS.exists_homogeneous_laplacian_of_higher_order line 75