OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingModeConverse.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.hasDerivAt_expandingMode_interaction line 11
2. theorem OAI.DefocusingNLS.expandingMode_variation_of_constants line 26
3. theorem OAI.DefocusingNLS.expandingMild_of_mode_equation line 55

   Source documentation

   Equality of all physical coefficients identifies the actual vector path. Only continuity at the slab endpoints is required there.

   theorem expandingMild_of_mode_equation (a b k L T : ℝ)
       (ha : 0 < a) (hk : 8 < k) (hL : 1 ≤ L)
       (u r : ℝ → FourierL2) (hu : ContinuousOn u (Icc 0 T)) (hr : ContinuousOn r (Icc 0 T))
       (hode : ∀ t ∈ Ioo 0 T, ∀ n : frequencyLattice,
         HasDerivAt (fun s => expandingFourierCoefficient a k (expandingRadius L s) (u s) n)
           (expandingModeRate a b L t n *
             expandingFourierCoefficient a k (expandingRadius L t) (u t) n +
             expandingFourierCoefficient a k (expandingRadius L t) (r t) n) t)
       (t : ℝ) (ht : t ∈ Icc 0 T) :
       u t = expandingFreeStep a b k L t ha hk hL ht.1 (u 0) +
         expandingDuhamel a b k L ha hk hL t r := by
   …

   Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingFourierCoefficient, OAI.DefocusingNLS.expandingRadius, OAI.DefocusingNLS.expandingModeRate, OAI.DefocusingNLS.expandingFreeStep, OAI.DefocusingNLS.expandingDuhamel