OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevCompactStability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.maximalSobolevSchrodingerFlow_compact_stability line 13

   Source documentation

   On every compact interval before the reference solution's maximal time, one neighborhood of its initial datum gives existence and uniform Sobolev closeness throughout that interval.

   theorem maximalSobolevSchrodingerFlow_compact_stability
       (k : ℝ) (hk : 6 < k) (m : ℕ) (f : FourierL2) (T ε : ℝ) (hε : 0 < ε)
       (hdom : T ∈ maximalSobolevInteractionDomain k hk m f) :
       ∃ δ : ℝ, 0 < δ ∧ ∀ g : FourierL2, dist g f < δ → ∀ t ∈ Icc 0 T,
         t ∈ maximalSobolevInteractionDomain k hk m g ∧
           dist (maximalSobolevSchrodingerFlow k hk m g t)
             (maximalSobolevSchrodingerFlow k hk m f t) < ε := by
   …

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

2. theorem OAI.DefocusingNLS.isOpen_maximalSobolev_terminal_condition line 50

   Source documentation

   Reaching a specified open set at a fixed forward time is an open condition on the datum.

   theorem isOpen_maximalSobolev_terminal_condition
       (k : ℝ) (hk : 6 < k) (m : ℕ) (T : ℝ) (hT : 0 ≤ T)
       (V : Set FourierL2) (hV : IsOpen V) :
       IsOpen {f : FourierL2 | T ∈ maximalSobolevInteractionDomain k hk m f ∧
         maximalSobolevSchrodingerFlow k hk m f T ∈ V} := by
   …

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