SobolevTranslation.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Spatial translations on the actual Fourier Sobolev space

def OAI.DefocusingNLS.sobolevTranslation line 14
Source documentation
Translation by x multiplies the Fourier coefficients by exp(i n·x).
```
noncomputable def sobolevTranslation (x : SchrodingerTorus) : FourierL2 →ₗᵢ[ℂ] FourierL2 where
…
```
Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.sobolevTranslation_apply line 27
theorem OAI.DefocusingNLS.sobolevTranslation_zero line 30
theorem OAI.DefocusingNLS.sobolevTranslation_add line 34
theorem OAI.DefocusingNLS.sobolevTorusFunction_translation line 40
Source documentation
The Fourier action represents translation of the continuous torus function.
```
theorem sobolevTorusFunction_translation (k : ℝ) (hk : 6 < k)
    (x y : SchrodingerTorus) (f : FourierL2) :
    sobolevTorusFunction k (sobolevTranslation x f) y = sobolevTorusFunction k f (x + y) := by
…
```
Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevTranslation
theorem OAI.DefocusingNLS.continuous_sobolevTranslation line 51
Source documentation
Strong continuity of spatial translation in every represented Sobolev order.
```
theorem continuous_sobolevTranslation (f : FourierL2) :
    Continuous (fun x : SchrodingerTorus => sobolevTranslation x f) := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.sobolevTranslation
theorem OAI.DefocusingNLS.continuous_sobolevTranslation_uncurry line 90
Source documentation
Spatial shifts and initial data vary jointly continuously in the Sobolev norm.
```
theorem continuous_sobolevTranslation_uncurry :
    Continuous (fun p : SchrodingerTorus × FourierL2 => sobolevTranslation p.1 p.2) := by
…
```
Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevTranslation