OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousOutgoingComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The high radial derivative detects the transverse outgoing defect

The exact Euler recurrence separates its velocity row from the outgoing remainder. Dividing by the physical derivative scaling gives the power comparison used with radial square integrability.

  1. theorem OAI.DefocusingNLS.homogeneousEulerRows_defect_identity line 22
  2. theorem OAI.DefocusingNLS.homogeneousLogRow_norm_comparison line 43
  3. theorem OAI.DefocusingNLS.homogeneousLogRow_energy_comparison line 72