OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/FiniteSymmetryDecomposition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The three actual symmetry eigenvalues give a concrete decomposition.

  1. theorem OAI.DefocusingNLS.symmetry_eigenspaces_sup_eq_top line 10
  2. theorem OAI.DefocusingNLS.symmetry_eigenvector_decomposition line 25
  3. theorem OAI.DefocusingNLS.symmetry_polynomial_annihilates line 39