OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralScalarFluxLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An explicit flux lower bound survives a small error in the weighted Cauchy data, with constants suitable for the outgoing WKB comparison.

  1. theorem OAI.DefocusingNLS.spectralScalarFlux_lower_of_close line 10