OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingOrderedConjugate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Real differentiation commutes with physical complex conjugation

  1. theorem OAI.DefocusingNLS.homogeneousOrderedSymbol_conjugate line 14
  2. theorem OAI.DefocusingNLS.expandingOrderedMultiplier_conjugate line 23
  3. theorem OAI.DefocusingNLS.expandingOrderedFourierEnergy_conjugate line 31