OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphEndpoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

From the graph contraction to the original endpoint sequence

The source identities below are the exact projected nonlinear remainder and coordinate defect. They permit the abstract contraction to reconstruct the original endpoint dynamics, with a prescribed stable initial coordinate.

  1. theorem OAI.DefocusingNLS.exists_stableGraph_endpoint_sequence line 19