OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowSlitDomination.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds near the nonzero imaginary spatial boundary

  1. theorem OAI.DefocusingNLS.norm_cpow_le_of_norm_bounds line 11
  2. theorem OAI.DefocusingNLS.one_add_real_div_bounds_of_im line 34
  3. theorem OAI.DefocusingNLS.slowKernelSpatialDerivative_majorant_of_im line 57
  4. theorem OAI.DefocusingNLS.exists_slowKernelSpatialDerivative_majorant_of_im line 108