OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffStepRemainder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual cutoff-step estimates in weighted sequence form

These adapters use exactly the remainder bounds proved for the sampled nonlinear step. The exponent along L exp(nM/2) is geometric, and the small Lipschitz constant is obtained by first reducing the state ball and then increasing the starting radius. The step maps themselves are not assumed to be spectral projections or a stable graph.

  1. theorem OAI.DefocusingNLS.expandingRadius_discrete_residual line 19
  2. theorem OAI.DefocusingNLS.exists_cutoffStep_geometric_ratio line 26
  3. def OAI.DefocusingNLS.cutoffRemainderExtension line 50
  4. theorem OAI.DefocusingNLS.cutoffRemainderExtension_lipschitz line 54
  5. theorem OAI.DefocusingNLS.cutoffRemainderExtension_zero_bound line 79
  6. theorem OAI.DefocusingNLS.exists_cutoffRemainder_small_lipschitz line 92