OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingSolutionContinuity.lean

Continuity of bounded actual mild-solution families

The local polynomial Lipschitz estimate is used only along the actual two solutions. Exponential weighting gives a uniform pair contraction, so continuity follows from continuity of the Picard map at a fixed path. No globally Lipschitz extension of the reaction is introduced.