OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingLocalDependence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-step dependence using only the two actual trajectories

The odd-power reaction need not be globally Lipschitz. A uniform bound on its difference along the two solutions gives the required finite-step Lipschitz estimate for their initial data.

  1. theorem OAI.DefocusingNLS.expandingBieleckiPicard_initial_dist_le line 18
  2. theorem OAI.DefocusingNLS.expandingMild_finiteSlab_local_data_bound line 42