OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteIncomingBootstrap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The incoming ODE improves an outgoing symbol by two powers per step. This proves the vanishing terminal condition used by the integral estimate.

  1. theorem OAI.DefocusingNLS.spectralRemote_incoming_bootstrap line 13