OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralGreenBranchBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Convert the piecewise Green bound to both closed integration intervals. At the diagonal the derivative jump contributes exactly one inverse weight.

  1. theorem OAI.DefocusingNLS.spectralGreen_diagonal_jump line 11
  2. theorem OAI.DefocusingNLS.spectralGreen_closed_branch_bounds line 22