OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningResidualUniform.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every fixed cutoff at least 32 gives a uniform bound for the forbidden residual. This bounds the Green constant along an escaping parameter sequence.

  1. theorem OAI.DefocusingNLS.spectralTurningCutoffError_le line 11
  2. theorem OAI.DefocusingNLS.spectralTurning_eventual_residual_bound line 24