OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingFilteredPhysicalEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Physical realization of a filtered ordered derivative

  1. theorem OAI.DefocusingNLS.expandingOrderedFourierEnergy_smoothLow line 18
  2. theorem OAI.DefocusingNLS.expandingOrderedPhysicalEnergy_smoothLow line 31
  3. theorem OAI.DefocusingNLS.torusL2Product_physical line 42