OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/StableGraphContinuity.lean

Continuity from uniformly contracting iterates

Only continuity of the observed finite iterates is required. In the stable graph application the observation is a single coordinate, whose continuity comes from strong Fourier continuity and uniformly convergent backward tails. Operator-norm continuity of the free Schrödinger group is unnecessary.