OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffContinuousLinearization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous nonlinear cutoff steps with the exact linear endpoint

  1. def OAI.DefocusingNLS.HasContinuousCutoffNonlinearSteps line 16
  2. theorem OAI.DefocusingNLS.exists_cutoffContinuousNonlinear_steps_order line 39