OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousRadialDefect.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact transverse defect of the outgoing value plane

The two-channel second-order equation gives a closed first-order equation for U' - A U whenever A satisfies its Riccati identity. This is the starting point for excluding a transverse component using the actual top-derivative L² bound.

  1. theorem OAI.DefocusingNLS.homogeneousPair_fst_hasDerivAt line 22
  2. theorem OAI.DefocusingNLS.homogeneousPair_snd_hasDerivAt line 26
  3. def OAI.DefocusingNLS.homogeneousRadialDamping line 30
  4. def OAI.DefocusingNLS.homogeneousRadialStiffness line 34
  5. theorem OAI.DefocusingNLS.homogeneousRadial_acceleration line 42
  6. theorem OAI.DefocusingNLS.homogeneousComplexOperator_hasDerivAt_apply line 55
  7. def OAI.DefocusingNLS.homogeneousRadialDefect line 63
  8. theorem OAI.DefocusingNLS.homogeneousRadialDefect_hasDerivAt line 66