SobolevRestartExtension.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Extending a maximal trajectory through a later local solution

theorem OAI.DefocusingNLS.maximalSobolevInteractionFlow_restart_extension line 13

Source documentation

A classical interaction solution through a later point extends the original maximal trajectory to the right. This is a gluing theorem, with no assumed continuation principle.

theorem maximalSobolevInteractionFlow_restart_extension
    (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2) (s δ : ℝ)
    (hs : s ∈ maximalSobolevInteractionDomain k hk m f₀) (hs₀ : 0 ≤ s) (hδ : 0 < δ)
    (w : ℝ → FourierL2)
    (hw : ∀ t ∈ Ioo (s - δ) (s + δ),
      HasDerivAt w (schrodingerInteractionField k hk m t (w t)) t)
    (hw₀ : w s = maximalSobolevInteractionFlow k hk m f₀ s) :
    ∀ t ∈ Ico s (s + δ),
      t ∈ maximalSobolevInteractionDomain k hk m f₀ ∧
        maximalSobolevInteractionFlow k hk m f₀ t = w t := by
…

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

theorem OAI.DefocusingNLS.maximalSobolevSchrodingerFlow_restart_extension line 81

Source documentation

A local physical solution through a later state extends the original maximal physical solution. The derivative is taken in the lower Sobolev space, as in the Cauchy problem.

theorem maximalSobolevSchrodingerFlow_restart_extension
    (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2) (s δ : ℝ)
    (hs : s ∈ maximalSobolevInteractionDomain k hk m f₀) (hs₀ : 0 ≤ s) (hδ : 0 < δ)
    (w : ℝ → FourierL2) (hw₀ : w 0 = maximalSobolevSchrodingerFlow k hk m f₀ s)
    (hwc : ContinuousOn w (Ioo (-δ) δ))
    (hw : ∀ t ∈ Ioo (-δ) δ, HasDerivAt (fun r => lowerSobolevInclusion (w r))
      (lowerSobolevGenerator (w t) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (w t))) t) :
    ∀ t ∈ Ico 0 δ,
      s + t ∈ maximalSobolevInteractionDomain k hk m f₀ ∧
        maximalSobolevSchrodingerFlow k hk m f₀ (s + t) = w t := by
…

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