OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousDefectComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact derivative-row comparison implies the radial L² obstruction

This is the quantitative two-channel inequality used after the falling-Euler row and the differentiated outgoing remainder have been identified.

  1. theorem OAI.DefocusingNLS.homogeneousPair_energy_control line 18
  2. theorem OAI.DefocusingNLS.homogeneousRadial_derivative_comparison line 42