SchrodingerTorus.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The free equation on the actual twelve-torus

The Fourier Sobolev model embeds continuously into continuous functions for k>6. For k>8, free evolution is differentiable in the continuous-function norm, and its derivative is i times the continuous Fourier Laplacian.

def OAI.DefocusingNLS.sobolevTorusEmbedding line 19
Source documentation
The Fourier representation is a bounded linear map into continuous functions.
```
noncomputable def sobolevTorusEmbedding (k : ℝ) (hk : 6 < k) :
    FourierL2 →L[ℂ] C(SchrodingerTorus, ℂ) :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus
theorem OAI.DefocusingNLS.sobolevTorusEmbedding_apply line 40
theorem OAI.DefocusingNLS.sobolevTorusFunction_lower_inclusion line 44
Source documentation
Lowering the index of a Sobolev vector preserves its continuous torus function.
```
theorem sobolevTorusFunction_lower_inclusion (k : ℝ) (f : FourierL2) :
    sobolevTorusFunction (k - 2) (lowerSobolevInclusion f) = sobolevTorusFunction k f := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.lowerSobolevInclusion
theorem OAI.DefocusingNLS.lowerSobolevInclusion_schrodingerFlow line 51
theorem OAI.DefocusingNLS.lowerSobolevGenerator_schrodingerFlow line 58
def OAI.DefocusingNLS.torusFourierLaplacian line 66
Source documentation
The spectral Laplacian, represented as a continuous function for k>8.
```
noncomputable def torusFourierLaplacian (k : ℝ) (f : FourierL2) :
    C(SchrodingerTorus, ℂ) :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus

theorem OAI.DefocusingNLS.sobolevFourierCoefficient_laplacian line 71

Source documentation

The Fourier Laplacian has precisely the multiplier -|n|².

theorem sobolevFourierCoefficient_laplacian (k : ℝ) (f : FourierL2)
    (n : frequencyLattice) :
    sobolevFourierCoefficient (k - 2) (-Complex.I • lowerSobolevGenerator f) n =
      -((‖n‖ ^ 2 : ℝ) : ℂ) * sobolevFourierCoefficient k f n := by
…

Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.sobolevFourierCoefficient

theorem OAI.DefocusingNLS.hasSum_torusFourierLaplacian line 86
Source documentation
The Laplacian Fourier series converges absolutely and defines the stated function.
```
theorem hasSum_torusFourierLaplacian (k : ℝ) (hk : 8 < k) (f : FourierL2)
    (x : SchrodingerTorus) :
    HasSum (fun n => -((‖n‖ ^ 2 : ℝ) : ℂ) * sobolevFourierCoefficient k f n *
      torusCharacter n x) (torusFourierLaplacian k f x) := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.sobolevFourierCoefficient, OAI.DefocusingNLS.torusCharacter, OAI.DefocusingNLS.torusFourierLaplacian
def OAI.DefocusingNLS.freeTorusEvolution line 96
Source documentation
The free evolution, represented by continuous functions on the torus.
```
noncomputable def freeTorusEvolution (k : ℝ) (f : FourierL2) (t : ℝ) :
    C(SchrodingerTorus, ℂ) := sobolevTorusFunction k (schrodingerFlow t f)
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus
theorem OAI.DefocusingNLS.hasDerivAt_freeTorusEvolution line 100
Source documentation
Free evolution solves the spectral Schrödinger equation in the continuous-function norm.
```
theorem hasDerivAt_freeTorusEvolution (k : ℝ) (hk : 8 < k) (f : FourierL2) (t : ℝ) :
    HasDerivAt (freeTorusEvolution k f)
      (Complex.I • torusFourierLaplacian k (schrodingerFlow t f)) t := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.freeTorusEvolution, OAI.DefocusingNLS.torusFourierLaplacian
theorem OAI.DefocusingNLS.hasDerivAt_freeTorusEvolution_point line 122
Source documentation
At every point of the torus, the time derivative equals i times the Fourier Laplacian.
```
theorem hasDerivAt_freeTorusEvolution_point (k : ℝ) (hk : 8 < k) (f : FourierL2)
    (x : SchrodingerTorus) (t : ℝ) :
    HasDerivAt (fun s => freeTorusEvolution k f s x)
      (Complex.I * torusFourierLaplacian k (schrodingerFlow t f) x) t := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.freeTorusEvolution, OAI.DefocusingNLS.torusFourierLaplacian