OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousOutgoingDefectZero.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Radial square integrability forces the outgoing defect to vanish

A nonzero defect has a fixed polynomial energy lower bound. The exact high-derivative comparison and the twelve-dimensional radial measure contradict that bound, even with the decaying outgoing remainder present.

  1. theorem OAI.DefocusingNLS.homogeneousOutgoingDefect_eq_zero line 18