SpectralTurningOutgoingConnection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual normalized outgoing solutions cross the turning region with a uniformly nonzero physical growing WKB coefficient. No Airy solution or matching coefficient is assumed as input.

theorem OAI.DefocusingNLS.spectralTurning_outgoing_growing_connection line 13