OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousMatchedObservation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual matched profile has a contracting essential time step

The integer differentiability order is chosen after the fixed power. Its principal coefficient is controlled by the proved global pressure bound; no decay or spectral estimate is assumed for the evolution.

  1. theorem OAI.DefocusingNLS.radialMatched_exists_weakNull_contraction line 21