OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousLinearizedSemigroup.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual homogeneous linearized semigroup

Finite-slab solutions agree on their common interval and restart at every nonnegative time. These identities give the strongly continuous evolution whose time-one map enters the finite-rank decomposition.

  1. def OAI.DefocusingNLS.homogeneousLinearizedStep line 24
  2. theorem OAI.DefocusingNLS.homogeneousLinearizedStep_eq_slab line 29
  3. theorem OAI.DefocusingNLS.homogeneousLinearizedStep_zero line 37
  4. theorem OAI.DefocusingNLS.homogeneousLinearizedStep_add line 47
  5. theorem OAI.DefocusingNLS.homogeneousLinearizedStep_nat line 65
  6. theorem OAI.DefocusingNLS.continuous_homogeneousLinearizedStep_apply line 76