OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningGreenSmallness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

In the regularized turning norm the full Green correction is bounded by a fixed constant times the vanishing Airy scale.

  1. theorem OAI.DefocusingNLS.spectralTurning_green_integral_bound line 13