OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevLocalContinuousFlow.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.exists_continuous_sobolevInteractionFlow_on_ball line 14

   Source documentation

   Every bounded ball of initial data has a jointly continuous interaction flow on a common positive time interval. The flow solves the actual polynomial interaction equation.

   theorem exists_continuous_sobolevInteractionFlow_on_ball
       (k : ℝ) (hk : 6 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
       ∃ δ : ℝ, 0 < δ ∧ ∃ α : FourierL2 × ℝ → FourierL2,
         ContinuousOn α (closedBall 0 R ×ˢ Icc (-δ) δ) ∧
         ∀ f : FourierL2, ‖f‖ ≤ R → α (f, 0) = f ∧
           ∀ t ∈ Ioo (-δ) δ, HasDerivAt (fun s => α (f, s))
             (schrodingerInteractionField k hk m t (α (f, t))) t := by
   …

   Mentions: OAI.DefocusingNLS.FourierL2

2. theorem OAI.DefocusingNLS.exists_continuous_maximalSobolevInteractionFlow_on_ball line 69

   Source documentation

   The local interaction map agrees with the maximal interaction flow on the common interval.

   theorem exists_continuous_maximalSobolevInteractionFlow_on_ball
       (k : ℝ) (hk : 6 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
       ∃ δ : ℝ, 0 < δ ∧
         (∀ f : FourierL2, ‖f‖ ≤ R →
           Ioo (-δ) δ ⊆ maximalSobolevInteractionDomain k hk m f) ∧
         ContinuousOn (fun p : FourierL2 × ℝ => maximalSobolevInteractionFlow k hk m p.1 p.2)
           (closedBall 0 R ×ˢ Ioo (-δ) δ) := by
   …

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

3. theorem OAI.DefocusingNLS.exists_continuous_maximalSobolevSchrodingerFlow_on_ball line 98

   Source documentation

   The actual maximal physical flow is jointly continuous in the datum and time on one common interval for every bounded ball of initial data.

   theorem exists_continuous_maximalSobolevSchrodingerFlow_on_ball
       (k : ℝ) (hk : 6 < k) (m : ℕ) (R : ℝ) (hR : 0 ≤ R) :
       ∃ δ : ℝ, 0 < δ ∧
         (∀ f : FourierL2, ‖f‖ ≤ R →
           Ioo (-δ) δ ⊆ maximalSobolevInteractionDomain k hk m f) ∧
         ContinuousOn (fun p : FourierL2 × ℝ => maximalSobolevSchrodingerFlow k hk m p.1 p.2)
           (closedBall 0 R ×ˢ Ioo (-δ) δ) := by
   …

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