OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevSymmetryFlow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.mapInteractionPatch line 12
2. theorem OAI.DefocusingNLS.maximalInteractionFlow_map line 28
3. theorem OAI.DefocusingNLS.schrodingerInteractionField_translation line 44
4. theorem OAI.DefocusingNLS.maximalSobolevInteractionDomain_translation line 51
5. theorem OAI.DefocusingNLS.maximalSobolevSchrodingerFlow_translation line 70

   Source documentation

   Translating the initial datum translates the maximal physical solution at every time.

   theorem maximalSobolevSchrodingerFlow_translation (k : ℝ) (hk : 6 < k) (m : ℕ)
       (x : SchrodingerTorus) (f : FourierL2) (t : ℝ)
       (ht : t ∈ maximalSobolevInteractionDomain k hk m f) :
       maximalSobolevSchrodingerFlow k hk m (sobolevTranslation x f) t =
         sobolevTranslation x (maximalSobolevSchrodingerFlow k hk m f t) := by
   …

   Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.maximalSobolevInteractionDomain, OAI.DefocusingNLS.sobolevTranslation

6. theorem OAI.DefocusingNLS.schrodingerInteractionField_phase line 84
7. theorem OAI.DefocusingNLS.sobolevPhase_inv_apply line 91
8. theorem OAI.DefocusingNLS.maximalSobolevInteractionDomain_phase line 96
9. theorem OAI.DefocusingNLS.maximalSobolevSchrodingerFlow_phase line 114

   Source documentation

   Unit phase commutes with the maximal physical flow and preserves its lifespan.

   theorem maximalSobolevSchrodingerFlow_phase (k : ℝ) (hk : 6 < k) (m : ℕ)
       (c : Circle) (f : FourierL2) (t : ℝ)
       (ht : t ∈ maximalSobolevInteractionDomain k hk m f) :
       maximalSobolevSchrodingerFlow k hk m (sobolevPhase c f) t =
         sobolevPhase c (maximalSobolevSchrodingerFlow k hk m f t) := by
   …

   Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.maximalSobolevInteractionDomain, OAI.DefocusingNLS.sobolevPhase