OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/MaximalStrongSolution.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.continuousOn_maximalSobolevSchrodingerFlow line 13
2. theorem OAI.DefocusingNLS.strongSobolevSchrodingerSolution_restricts_maximal line 22

   Source documentation

   Every strong solution through the initial datum is a restriction of the maximal flow.

   theorem strongSobolevSchrodingerSolution_restricts_maximal
       (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2)
       (u : ℝ → FourierL2) (a b : ℝ) (ha : a < 0) (hb : 0 < b)
       (hu₀ : u 0 = f₀) (huc : ContinuousOn u (Ioo a b))
       (hu : ∀ t ∈ Ioo a b, HasDerivAt (fun s => lowerSobolevInclusion (u s))
         (lowerSobolevGenerator (u t) -
           Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u t))) t) :
       Ioo a b ⊆ maximalSobolevInteractionDomain k hk m f₀ ∧
         EqOn u (maximalSobolevSchrodingerFlow k hk m f₀) (Ioo a b) := by
   …

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

3. theorem OAI.DefocusingNLS.maximalSobolev_lifespan_of_positive_rescaled_observation line 48

   Source documentation

   A positive rescaled observation fixes the finite endpoint of the maximal strong solution. The observation may be evaluation at any point of the twelve-dimensional torus.

   theorem maximalSobolev_lifespan_of_positive_rescaled_observation
       {F : Type*} [NormedAddCommGroup F]
       (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2)
       (u : ℝ → FourierL2) (a T β c : ℝ) (ha : a < 0) (hT : 0 < T)
       (hβ : 0 < β) (hc : 0 < c) (hu₀ : u 0 = f₀)
       (huc : ContinuousOn u (Ioo a T))
       (hu : ∀ t ∈ Ioo a T, HasDerivAt (fun s => lowerSobolevInclusion (u s))
         (lowerSobolevGenerator (u t) -
           Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u t))) t)
       (observe : FourierL2 → F) (hobs : Continuous observe)
       (hblowup : Tendsto (fun t => (T - t) ^ β * ‖observe (u t)‖)
         (𝓝[<] T) (𝓝 c)) :
   …

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