OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralShellMatchedCoupling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The small coefficient in the shell Green argument is supplied by the actual matched profile, uniformly in both spectral and angular parameters.

  1. def OAI.DefocusingNLS.spectralShellPlusForcing line 13
  2. def OAI.DefocusingNLS.spectralShellMinusForcing line 19
  3. theorem OAI.DefocusingNLS.spectralShellForcing_bound line 25
  4. theorem OAI.DefocusingNLS.radialMatched_shell_forcing_bound line 47