OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffMildEquation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The genuine sampled cutoff profile is a forced mild solution

  1. theorem OAI.DefocusingNLS.expandingModeRate_eq_radius line 15
  2. theorem OAI.DefocusingNLS.hasDerivAt_sampledCutoffProfileHistory_coefficient line 31
  3. theorem OAI.DefocusingNLS.sampledCutoffProfile_mild line 87