SobolevTimeTranslation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Time translation and restarting the strong Schrödinger flow

theorem OAI.DefocusingNLS.hasDerivAt_schrodinger_timeTranslation line 12

Source documentation

The strong physical equation is autonomous, so translating time preserves it.

theorem hasDerivAt_schrodinger_timeTranslation
    (k : ℝ) (hk : 6 < k) (m : ℕ) (u : ℝ → FourierL2) (s t : ℝ)
    (hu : HasDerivAt (fun r => lowerSobolevInclusion (u r))
      (lowerSobolevGenerator (u (s + t)) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u (s + t)))) (s + t)) :
    HasDerivAt (fun r => lowerSobolevInclusion (u (s + r)))
      (lowerSobolevGenerator (u (s + t)) -
        Complex.I • lowerSobolevInclusion (sobolevOddPower k hk m (u (s + t)))) t := by
…

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

theorem OAI.DefocusingNLS.continuousOn_timeTranslation line 23

theorem OAI.DefocusingNLS.strongSobolev_timeTranslation_restricts_maximal line 32

Source documentation

A translated strong solution is a restriction of the maximal flow through its new datum.

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

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

theorem OAI.DefocusingNLS.maximalSobolevSchrodingerFlow_local_restart line 51

Source documentation

At every time of a maximal trajectory, the local flow through its value agrees with the original trajectory on an open interval about that time.

theorem maximalSobolevSchrodingerFlow_local_restart
    (k : ℝ) (hk : 6 < k) (m : ℕ) (f₀ : FourierL2) (s : ℝ)
    (hs : s ∈ maximalSobolevInteractionDomain k hk m f₀) :
    ∃ a b : ℝ, a < 0 ∧ 0 < b ∧
      Ioo a b ⊆ maximalSobolevInteractionDomain k hk m
        (maximalSobolevSchrodingerFlow k hk m f₀ s) ∧
      ∀ t ∈ Ioo a b,
        s + t ∈ maximalSobolevInteractionDomain k hk m f₀ ∧
        maximalSobolevSchrodingerFlow k hk m f₀ (s + t) =
          maximalSobolevSchrodingerFlow k hk m
            (maximalSobolevSchrodingerFlow k hk m f₀ s) t := by
…

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