OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousLogCoefficients.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual radial coefficients satisfy the finite Euler-row bounds

In logarithmic radius, the normalized profile contributes bounded jets. The sole growing coefficient is the explicit Schrödinger diagonal.

  1. def OAI.DefocusingNLS.homogeneousLogFastDiagonal line 22
  2. def OAI.DefocusingNLS.homogeneousLogRadialDamping line 25
  3. def OAI.DefocusingNLS.homogeneousLogRadialStiffness line 28
  4. theorem OAI.DefocusingNLS.homogeneousLogFastDiagonal_norm line 37
  5. theorem OAI.DefocusingNLS.HasLogJetBound.spectralDiagonal line 45
  6. theorem OAI.DefocusingNLS.HasLogJetBound.spectralCross line 52
  7. theorem OAI.DefocusingNLS.homogeneousLogRadialStiffness_bound line 62
  8. theorem OAI.DefocusingNLS.radialExteriorCanonical_logJetBound line 87
  9. theorem OAI.DefocusingNLS.homogeneousPhysicalProfile_logJetBound line 96
  10. theorem OAI.DefocusingNLS.homogeneousCanonicalEulerRows_norm_lower line 105