OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialComplexSpectralEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact energy identity for complex spectral parameters.

Four real functions encode the real and imaginary parts of the two independent components. The imaginary spectral parameter cancels by Green symmetry.

  1. theorem OAI.DefocusingNLS.radialComplexSpectral_energy line 16