OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningBoundaryCoercive.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every normalized outgoing scalar comparison has a strictly inward logarithmic slope on a fixed inner sphere along an escaping turn.

  1. theorem OAI.DefocusingNLS.spectralTurning_normalized_inward line 12