OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevContinuousDependence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.exists_sobolevInteraction_gronwall_constant line 13

   Source documentation

   On a fixed norm ball, one exponential bound applies to all interaction trajectories.

   theorem exists_sobolevInteraction_gronwall_constant
       (k : ℝ) (hk : 6 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
       ∃ K : ℝ≥0, ∀ (v w : ℝ → FourierL2) (a b : ℝ),
         (∀ t ∈ Icc a b, HasDerivAt v (schrodingerInteractionField k hk m t (v t)) t) →
         (∀ t ∈ Icc a b, HasDerivAt w (schrodingerInteractionField k hk m t (w t)) t) →
         (∀ t ∈ Icc a b, ‖v t‖ ≤ R) → (∀ t ∈ Icc a b, ‖w t‖ ≤ R) →
         ∀ t ∈ Icc a b, dist (v t) (w t) ≤ dist (v a) (w a) * Real.exp (K * (t - a)) := by
   …

   Mentions: OAI.DefocusingNLS.FourierL2

2. theorem OAI.DefocusingNLS.exists_sobolevSchrodinger_gronwall_constant line 49

   Source documentation

   The same exponential estimate holds for strong physical Schrödinger solutions.

   theorem exists_sobolevSchrodinger_gronwall_constant
       (k : ℝ) (hk : 6 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
       ∃ K : ℝ≥0, ∀ (u v : ℝ → FourierL2) (a' b' a b : ℝ),
         Icc a b ⊆ Ioo a' b' →
         ContinuousOn u (Ioo a' b') → ContinuousOn v (Ioo a' b') →
         (∀ t ∈ Ioo a' b', HasDerivAt (fun s => lowerSobolevInclusion (u s))
           (lowerSobolevGenerator (u t) -
             Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u t))) t) →
         (∀ t ∈ Ioo a' b', HasDerivAt (fun s => lowerSobolevInclusion (v s))
           (lowerSobolevGenerator (v t) -
             Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (v t))) t) →
         (∀ t ∈ Icc a b, ‖u t‖ ≤ R) → (∀ t ∈ Icc a b, ‖v t‖ ≤ R) →
   …

   Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.lowerSobolevInclusion