OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingProfileEquation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.hasDerivAt_expandingProfileTrajectory_coefficient line 14

   Source documentation

   The constructed propagator has the prescribed real-linearized potential in every physical Fourier mode. Time is differentiated at fixed normalized torus position.

   theorem hasDerivAt_expandingProfileTrajectory_coefficient
       (a b k L T : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
       (hL : 1 ≤ L) (hT : 0 ≤ T) (m : ℕ) (R : ℝ) (hR : 0 ≤ R)
       (q : C(Icc (0 : ℝ) T, FourierL2)) (hq : ∀ t, ‖q t‖ ≤ R)
       (u₀ : FourierL2) (t : ℝ) (ht : t ∈ Ioo 0 T) (n : frequencyLattice) :
       let S := expandingProfileTrajectory a b k L T ha ha1 hk hL hT m R hR q hq u₀
   …

   Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.expandingProfileTrajectory