SobolevWeights.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Summability of the twelve-dimensional Gaussian Sobolev variances

The exponent restriction in Corollary 1.2 is exactly α > k + 6. We use the Euclidean integer lattice, defined as the integer span of the standard orthonormal basis, and the existing lattice p-series theorem.

def OAI.DefocusingNLS.frequencyLattice line 18
Source documentation
The standard Fourier frequency lattice in twelve dimensions.
Also declared: ComparatorChallenges/DefocusingNLS.lean:22 (same declaration text).
```
noncomputable def frequencyLattice : Submodule ℤ (EuclideanSpace ℝ (Fin 12)) :=
…
```
instance OAI.DefocusingNLS.(instance at line 21) line 21
instance OAI.DefocusingNLS.(instance at line 25) line 25
theorem OAI.DefocusingNLS.frequencyLattice_rank line 30
Source documentation
The frequency lattice has integer rank twelve.
```
theorem frequencyLattice_rank : Module.finrank ℤ frequencyLattice = 12 := by
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice
theorem OAI.DefocusingNLS.summable_sobolev_variances line 36
Source documentation
The square Sobolev weights of the Gaussian coefficients are summable. The lattice norm here is the Euclidean norm, as in the manuscript.
```
theorem summable_sobolev_variances (k α : ℝ) (hα : k + 6 < α) :
    Summable (fun n : frequencyLattice => (1 + ‖n‖ ^ 2) ^ (k - α)) := by
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice