OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingPhysicalTrajectory.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.strictMono_expandingFreeTime line 12
2. theorem OAI.DefocusingNLS.expanding_clock_denominator_pos line 20
3. theorem OAI.DefocusingNLS.expandingInverseClock_mem_Icc line 32
4. theorem OAI.DefocusingNLS.expandingInverseClock_mem_Ioo line 44
5. def OAI.DefocusingNLS.expandingSchrodingerTrajectory line 56
6. theorem OAI.DefocusingNLS.expandingSchrodingerTrajectory_zero line 63
7. theorem OAI.DefocusingNLS.continuousOn_expandingSchrodingerTrajectory line 72
8. theorem OAI.DefocusingNLS.hasDerivAt_expandingSchrodingerTrajectory line 91
9. theorem OAI.DefocusingNLS.expandingSchrodingerTrajectory_eq_maximal line 123

   Source documentation

   The actual Picard trajectory, after exact time/amplitude/weight conversion, is the unique maximal Sobolev Schrödinger solution on its forward slab.

   theorem expandingSchrodingerTrajectory_eq_maximal (a b k L S : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (hS : 0 < S)
       (m : ℕ) (ham : 2 * a * m = 1)
       (u : C(Icc (0 : ℝ) S, FourierL2)) (u₀ : FourierL2)
       (hu : u = expandingPicard a b k L S ha hk hL hS.le
         (expandingNonlinearReaction a k L S ha ha1 hk hL m) u₀ u) :
       let U := expandingSchrodingerTrajectory a b k L S ha ha1 hk hL hS.le u
   …

   Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingPicard, OAI.DefocusingNLS.expandingNonlinearReaction, OAI.DefocusingNLS.expandingSchrodingerTrajectory