OAI/MathematicalPhysics/DefocusingNLS/Certificates/FreePhysicalGeneralizedExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The physical free boundary problem has no first generalized eigenvector at a symmetry root, assuming the rectangle form of Rouché's theorem.

  1. theorem OAI.DefocusingNLS.radialFreePhysical_generalized_exclusion line 15