OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffPathContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Scale continuity of the actual sampled cutoff histories

The smooth profile and exact cutoff residual vary continuously in the finite-time path norm. This supplies the concrete parameter hypotheses for the nonlinear step continuity theorem.

  1. theorem OAI.DefocusingNLS.continuous_sampledCutoffProfilePath line 20
  2. theorem OAI.DefocusingNLS.continuous_sampledCutoffResidualPath line 30
  3. theorem OAI.DefocusingNLS.continuous_sampledCutoffDefectPath line 42