OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousMatchedGenerator.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional generator for the actual matched profile

This is the concrete semigroup conclusion preceding identification of its finite-dimensional modes with the symmetry modes.

  1. theorem OAI.DefocusingNLS.radialMatched_exists_finite_generator line 21