OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralWKBDecreasingIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reflection gives the endpoint form for decreasing momentum, as used on the forbidden side of a turning point.

  1. theorem OAI.DefocusingNLS.spectralWKB_decreasing_residual_integral line 11