OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphContraction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A Banach contraction for the forward/backward recurrence

All inputs are explicit estimates on the two linear blocks and the two nonlinear remainder maps. This is the recurrence lemma used by nl:graph, not an assumption of the spectral splitting or the stable graph itself. The mixed block is small after weighting the finite-dimensional coordinates.

  1. def OAI.DefocusingNLS.stableGraphMap line 23
  2. theorem OAI.DefocusingNLS.stableGraphMap_dist_le line 33
  3. theorem OAI.DefocusingNLS.stableGraphMap_zero_bound line 54
  4. theorem OAI.DefocusingNLS.exists_stableGraph_fixedPoint line 71