OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousHarmonicEigenL2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted radial L² control of actual generator eigenmodes

Smoothness is derived from the projected ODE, and the top radial derivative is then identified with the completed Cartesian derivative contraction.

  1. theorem OAI.DefocusingNLS.homogeneous_eigenvector_harmonic_topL2 line 19