OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousLinearizedFlow.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Bounded real-linear propagators for the actual profile potential

The potential is the Fréchet derivative of the actual odd-power map at q. Its finite-slab trajectory is linear in the data, quantitatively bounded, and jointly continuous in the elapsed time and the initial vector.

  1. def OAI.DefocusingNLS.homogeneousLinearizedTrajectory line 25
  2. theorem OAI.DefocusingNLS.homogeneousLinearizedTrajectory_eq line 32
  3. theorem OAI.DefocusingNLS.homogeneousLinearizedTrajectory_unique line 39
  4. theorem OAI.DefocusingNLS.linearized_history_zero line 47
  5. theorem OAI.DefocusingNLS.linearized_history_add line 51
  6. theorem OAI.DefocusingNLS.linearized_history_smul line 57
  7. theorem OAI.DefocusingNLS.homogeneousLinearizedTrajectory_zero line 63
  8. theorem OAI.DefocusingNLS.homogeneousLinearizedTrajectory_add line 71
  9. theorem OAI.DefocusingNLS.homogeneousLinearizedTrajectory_smul line 85
  10. theorem OAI.DefocusingNLS.homogeneousLinearizedTrajectory_norm_le line 95
  11. def OAI.DefocusingNLS.homogeneousLinearizedPropagator line 105
  12. theorem OAI.DefocusingNLS.homogeneousLinearizedPropagator_apply line 114
  13. theorem OAI.DefocusingNLS.homogeneousLinearizedPropagator_norm_le line 117
  14. theorem OAI.DefocusingNLS.continuous_homogeneousLinearizedPropagator_apply line 123