SobolevTranslationEquation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Translation covariance of the strong nonlinear Schrödinger equation

theorem OAI.DefocusingNLS.sobolevFourierCoefficient_translation line 12
theorem OAI.DefocusingNLS.sobolevProduct_translation line 19
theorem OAI.DefocusingNLS.fourierConjugate_translation line 45
theorem OAI.DefocusingNLS.sobolevOddPower_translation line 51
Source documentation
Translation commutes with the actual polynomial Sobolev nonlinearity.
```
theorem sobolevOddPower_translation (k : ℝ) (hk : 6 < k) (m : ℕ)
    (x : SchrodingerTorus) (f : FourierL2) :
    sobolevOddPower k hk m (sobolevTranslation x f) =
      sobolevTranslation x (sobolevOddPower k hk m f) := by
…
```
Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevTranslation
theorem OAI.DefocusingNLS.lowerSobolevInclusion_translation line 60
theorem OAI.DefocusingNLS.lowerSobolevGenerator_translation line 67
theorem OAI.DefocusingNLS.schrodingerFlow_translation line 74

theorem OAI.DefocusingNLS.hasDerivAt_sobolevSchrodinger_translation line 82

Source documentation

Spatially translated strong solutions satisfy the same defocusing equation.

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

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