OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousWeakGenerator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The weak Fourier equation for the actual free generator

This is the distributional identity behind the physical operator i Delta - x dot grad / 2 - a + i b. The statement uses ordinary Lebesgue integrals of the faithful Fourier representative and Schwartz tests.

  1. theorem OAI.DefocusingNLS.hasDerivAt_homogeneousFourierPairing_free line 22
  2. theorem OAI.DefocusingNLS.homogeneousFree_weak_generator line 62