ExpandingFourier.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The exact Y_L Fourier realization and uniform ℓ¹ embedding

def OAI.DefocusingNLS.expandingFourierCoefficient line 14
Source documentation
Physical Fourier coefficients for a vector whose ℓ² norm is the exact Y_L norm.
```
noncomputable def expandingFourierCoefficient (a k L : ℝ) (f : FourierL2)
    (n : frequencyLattice) : ℂ :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice
theorem OAI.DefocusingNLS.weight_mul_expandingFourierCoefficient line 18

theorem OAI.DefocusingNLS.expandingFourier_norm_sq line 27

Source documentation

The Hilbert norm equals the manuscript's volume-weighted Fourier norm exactly.

theorem expandingFourier_norm_sq (a k L : ℝ) (hL : 1 ≤ L) (f : FourierL2) :
    (2 * Real.pi * L) ^ 12 * (∑' n : frequencyLattice,
      ((L ^ (-2 : ℝ) + (‖n‖ / L) ^ 2) ^ (6 - a) + (‖n‖ / L) ^ (2 * k)) *
        ‖expandingFourierCoefficient a k L f n‖ ^ 2) = ‖f‖ ^ 2 := by
…

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

theorem OAI.DefocusingNLS.expanding_observation_weight_sq line 50
def OAI.DefocusingNLS.expandingObservationVector line 59
Source documentation
Inverse weights form an ℓ² vector with a uniform norm as the torus expands.
```
noncomputable def expandingObservationVector (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
def OAI.DefocusingNLS.expandingEmbeddingBound line 68
theorem OAI.DefocusingNLS.expandingObservationVector_norm_le line 72
theorem OAI.DefocusingNLS.hasSum_expandingFourierCoefficient line 96
theorem OAI.DefocusingNLS.summable_norm_expandingFourierCoefficient line 104
theorem OAI.DefocusingNLS.expandingFourierCoefficient_absolute line 109
theorem OAI.DefocusingNLS.tsum_norm_expandingFourierCoefficient_le line 118
Source documentation
The ℓ¹ Fourier embedding constant is independent of the expanding scale.
```
theorem tsum_norm_expandingFourierCoefficient_le (a k L : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (f : FourierL2) :
    (∑' n, ‖expandingFourierCoefficient a k L f n‖) ≤ expandingEmbeddingBound a k * ‖f‖ := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingFourierCoefficient, OAI.DefocusingNLS.expandingEmbeddingBound