OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFreeGroup.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Group law for the exact whole-space free evolution

  1. theorem OAI.DefocusingNLS.homogeneousFreeAmplitude_zero line 13
  2. theorem OAI.DefocusingNLS.homogeneousFreePhase_zero line 17
  3. theorem OAI.DefocusingNLS.homogeneousFreeAmplitude_add line 20
  4. theorem OAI.DefocusingNLS.homogeneousFreePhase_add line 29
  5. theorem OAI.DefocusingNLS.homogeneousFreeFourier_zero line 42
  6. theorem OAI.DefocusingNLS.homogeneousFreeFourier_add line 47
  7. theorem OAI.DefocusingNLS.homogeneousFreeOperator_zero line 60
  8. theorem OAI.DefocusingNLS.homogeneousFreeOperator_add line 70
  9. theorem OAI.DefocusingNLS.homogeneousFreeOperator_neg_cancel line 84