OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningFluxCoarse.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform constants for the outgoing flux estimate when the spectral imaginary part stays in the prescribed strip.

  1. def OAI.DefocusingNLS.spectralTurningFluxBase line 11
  2. def OAI.DefocusingNLS.spectralTurningFluxErrorConstant line 12
  3. def OAI.DefocusingNLS.spectralTurningFluxRemoteConstant line 15
  4. def OAI.DefocusingNLS.spectralTurningFluxNormConstant line 17
  5. theorem OAI.DefocusingNLS.spectralTurningFluxBase_pos line 19
  6. theorem OAI.DefocusingNLS.spectralTurning_flux_coarse line 23