OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialFreeModulus.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Modulus monotonicity and the exact normalization factor for the outgoing free H solution.

  1. theorem OAI.DefocusingNLS.complex_normSq_log_derivative line 11
  2. theorem OAI.DefocusingNLS.radialFreeRaw_norm_antitone line 25
  3. theorem OAI.DefocusingNLS.radialFreeSlow_cpow_norm line 70
  4. theorem OAI.DefocusingNLS.radialFreeSlowValue_norm line 84
  5. theorem OAI.DefocusingNLS.radialFreeSlowValue_norm_antitone line 101