OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousPhysicalLaplacian.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The classical gradient and Laplacian of the actual Y realization

  1. theorem OAI.DefocusingNLS.fderiv_homogeneousPhysical line 14
  2. theorem OAI.DefocusingNLS.integrable_physicalSquare line 23
  3. theorem OAI.DefocusingNLS.laplacian_homogeneousPhysical line 47