OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousMatchedPotential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The matched stationary profile supplies the actual whole-space evolution

The Y representative is obtained from the proved profile symbol estimates. Its bounded real-linear potential has exactly the two physical coefficients in the manuscript, and its finite-slab propagators have explicit bounds.

  1. theorem OAI.DefocusingNLS.exists_matched_homogeneousLinearized_propagator line 20