ExpandingTorus.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform point observation for the expanding-torus norm

Torus coordinates are normalized by the expanding scale. The coefficient norm is exactly the volume-weighted Y_L norm, with no change of Fourier weight.

def OAI.DefocusingNLS.expandingTorusTerm line 16
theorem OAI.DefocusingNLS.summable_expandingTorusTerm line 20
def OAI.DefocusingNLS.expandingTorusFunction line 27
theorem OAI.DefocusingNLS.expandingTorusFunction_apply line 30
theorem OAI.DefocusingNLS.tendstoUniformly_expandingFourierSeries line 43
Source documentation
Uniform convergence of the actual Fourier polynomials in normalized coordinates.
```
theorem tendstoUniformly_expandingFourierSeries (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (f : FourierL2) :
    TendstoUniformly
      (fun S : Finset frequencyLattice => fun x : SchrodingerTorus =>
        ∑ n ∈ S, expandingFourierCoefficient a k L f n * torusCharacter n x)
      (expandingTorusFunction a k L f) atTop := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.SchrodingerTorus, OAI.DefocusingNLS.expandingFourierCoefficient, OAI.DefocusingNLS.torusCharacter, OAI.DefocusingNLS.expandingTorusFunction
theorem OAI.DefocusingNLS.expandingTorusFunction_norm_le line 59
Source documentation
The observation constant is independent of the torus radius.
```
theorem expandingTorusFunction_norm_le (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (f : FourierL2) :
    ‖expandingTorusFunction a k L f‖ ≤ expandingEmbeddingBound a k * ‖f‖ := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingTorusFunction, OAI.DefocusingNLS.expandingEmbeddingBound
theorem OAI.DefocusingNLS.expandingTorusFunction_point_bound line 71