OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRobinRelative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Relative Robin errors separate into the propagated cone error and the explicit logarithmic derivative of the WKB amplitude.

  1. theorem OAI.DefocusingNLS.spectralRobin_relative_residual line 10
  2. theorem OAI.DefocusingNLS.spectralTurning_log_correction_bound line 26