OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphSelection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Initial stable coordinates select a Lipschitz graph

This selects the unique small fixed sequence of the contracting recurrence map. Its zeroth unstable coordinate is Lipschitz in the prescribed stable data. The torus spectral blocks and endpoint remainder estimates are hypotheses of this construction.

  1. theorem OAI.DefocusingNLS.stableGraphMap_initial_dist_le line 22
  2. theorem OAI.DefocusingNLS.stableGraph_fixedPoint_data_dist_le line 42
  3. theorem OAI.DefocusingNLS.exists_stableGraph_selection line 65