OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralPhysicalGoodPoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The normalized physical shell energy supplies bounded Cauchy data at a point in the first half of the shell.

  1. theorem OAI.DefocusingNLS.spectralPhysicalShell_good_point line 12