OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialComplexDilationIdentity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual coupled eigenvalue equation tested against the shifted dilation. The bulk scalar forms retain their exact outer boundary contribution.

  1. def OAI.DefocusingNLS.radialComplexDilationPairing line 14
  2. theorem OAI.DefocusingNLS.radialMatched_complex_dilation_identity line 19