OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphCoordinateContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Coordinate continuity of the graph iteration

The backward tail is uniformly geometric. Therefore continuity of each forcing coordinate suffices, without continuity in the sequence sup norm. Together with continuous_contraction_observation, this supplies the continuity mechanism stated in the manuscript's graph construction.

  1. theorem OAI.DefocusingNLS.continuous_stableBackward_coordinate line 18
  2. theorem OAI.DefocusingNLS.continuous_stableForward_coordinate line 38