OAI/MathematicalPhysics/DefocusingNLS/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Stable blowup for the defocusing Schrödinger equation
Arbitrarily large odd powers admit a nonempty open family of classical solutions on the twelve-dimensional torus with finite-time self-similar blowup. For the same power and integer Sobolev order above eight, every Gaussian decay exponent above that order plus six has positive blowup probability.
The construction combines radial profiles, spectral classification, decay on expanding tori, nonlinear stable graphs, physical-data openness and Gaussian full support.
This file declares nothing itself. It gathers the 6 imports below, so a file that imports it gets all of them.