SobolevTorus.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Continuous functions on the twelve-dimensional torus

The integer coordinates of the Euclidean frequency lattice define genuine periodic Fourier characters. Absolute summability gives a uniformly convergent Fourier representation, with bounded point evaluation at every torus point.

abbrev OAI.DefocusingNLS.SchrodingerTorus line 19
Also declared: ComparatorChallenges/DefocusingNLS.lean:76 (same declaration text).
instance OAI.DefocusingNLS.(instance at line 21) line 21
def OAI.DefocusingNLS.frequencyCoordinates line 24
Source documentation
Integer coordinates in the standard Euclidean Fourier lattice.
Also declared: ComparatorChallenges/DefocusingNLS.lean:80 (same declaration text).
```
noncomputable def frequencyCoordinates (n : frequencyLattice) : Fin 12 → ℤ :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice
def OAI.DefocusingNLS.torusCharacter line 28
Source documentation
The periodic character exp(i n·x).
Also declared: ComparatorChallenges/DefocusingNLS.lean:83 (same declaration text).
```
noncomputable def torusCharacter (n : frequencyLattice) : C(SchrodingerTorus, ℂ) where
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.SchrodingerTorus
theorem OAI.DefocusingNLS.torusCharacter_norm_apply line 32
theorem OAI.DefocusingNLS.torusCharacter_zero line 36
theorem OAI.DefocusingNLS.torusCharacter_norm line 39
def OAI.DefocusingNLS.sobolevTorusTerm line 45
Source documentation
A weighted Fourier coefficient times its periodic character.
Also declared: ComparatorChallenges/DefocusingNLS.lean:87 (same declaration text).
```
noncomputable def sobolevTorusTerm (k : ℝ) (f : FourierL2) (n : frequencyLattice) :
    C(SchrodingerTorus, ℂ) :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.SchrodingerTorus
theorem OAI.DefocusingNLS.summable_sobolevTorusTerm line 49
def OAI.DefocusingNLS.sobolevTorusFunction line 56
Source documentation
The actual continuous periodic function represented by a Fourier Sobolev vector.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:91 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.sobolevTorusFunction@path.
```
noncomputable def sobolevTorusFunction (k : ℝ) (f : FourierL2) : C(SchrodingerTorus, ℂ) :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.SchrodingerTorus
theorem OAI.DefocusingNLS.hasSum_sobolevTorusTerm line 59
theorem OAI.DefocusingNLS.tendstoUniformly_sobolevFourierSeries line 64
Source documentation
Fourier polynomials converge uniformly on the whole twelve-torus.
```
theorem tendstoUniformly_sobolevFourierSeries (k : ℝ) (hk : 6 < k) (f : FourierL2) :
    TendstoUniformly
      (fun S : Finset frequencyLattice => fun x : SchrodingerTorus =>
        ∑ n ∈ S, sobolevFourierCoefficient k f n * torusCharacter n x)
      (sobolevTorusFunction k f) atTop := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.sobolevFourierCoefficient, OAI.DefocusingNLS.torusCharacter
def OAI.DefocusingNLS.sobolevPointObservationVector line 79
Source documentation
The modulated inverse weights representing evaluation at x.
```
noncomputable def sobolevPointObservationVector (k : ℝ) (hk : 6 < k)
    (x : SchrodingerTorus) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.FourierL2
def OAI.DefocusingNLS.sobolevPointEvaluation line 88
Source documentation
Point evaluation is a continuous complex-linear functional on the Fourier Sobolev model.
```
noncomputable def sobolevPointEvaluation (k : ℝ) (hk : 6 < k)
    (x : SchrodingerTorus) : FourierL2 →L[ℂ] ℂ :=
…
```
Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.hasSum_sobolevPointEvaluation line 92
theorem OAI.DefocusingNLS.sobolevTorusFunction_apply line 102
Source documentation
The continuous Fourier function agrees with bounded point evaluation.
```
theorem sobolevTorusFunction_apply (k : ℝ) (hk : 6 < k) (x : SchrodingerTorus)
    (f : FourierL2) : sobolevTorusFunction k f x = sobolevPointEvaluation k hk x f := by
…
```
Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevPointEvaluation
theorem OAI.DefocusingNLS.sobolevPointObservationVector_norm line 112
Source documentation
The norm of the evaluation vector does not depend on the torus point.
```
theorem sobolevPointObservationVector_norm (k : ℝ) (hk : 6 < k) (x : SchrodingerTorus) :
    ‖sobolevPointObservationVector k hk x‖ = ‖sobolevObservationVector k hk‖ := by
…
```
Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.sobolevPointObservationVector, OAI.DefocusingNLS.sobolevObservationVector
theorem OAI.DefocusingNLS.sobolevPointEvaluation_bound line 128
Source documentation
The pointwise Sobolev embedding bound is uniform in x.
```
theorem sobolevPointEvaluation_bound (k : ℝ) (hk : 6 < k)
    (x : SchrodingerTorus) (f : FourierL2) :
    ‖sobolevPointEvaluation k hk x f‖ ≤ ‖sobolevObservationVector k hk‖ * ‖f‖ := by
…
```
Mentions: OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.sobolevPointEvaluation, OAI.DefocusingNLS.sobolevObservationVector

theorem OAI.DefocusingNLS.no_sobolev_extension_of_positive_point_rate line 136

Source documentation

Blowup at any point of the actual torus prevents Sobolev continuation.

theorem no_sobolev_extension_of_positive_point_rate
    (k : ℝ) (hk : 6 < k) (x : SchrodingerTorus) (u : ℝ → FourierL2)
    (T a c : ℝ) (ha : 0 < a) (hc : 0 < c)
    (hblowup : Tendsto (fun t => (T - t) ^ a * ‖sobolevTorusFunction k (u t) x‖)
      (𝓝[<] T) (𝓝 c)) : ¬ ContinuousWithinAt u (Set.Iio T) T := by
…

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