OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralBoundedFrameTerminal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bounded approximate oscillatory frame controls true solutions from their terminal data. The bound uses the integrated residual, uniformly over every subinterval.

  1. theorem OAI.DefocusingNLS.spectral_bounded_frame_terminal_bound line 13