GaussianFourier.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Almost-sure Sobolev summability of the Gaussian Fourier coefficients

The underlying independent coefficients are constructed using Mathlib's countable product measure. Their weighted square sum is almost surely finite at the exact threshold α > k + 6 from Corollary 1.2.

def OAI.DefocusingNLS.fourierGaussianLaw line 23
Source documentation
The standard independent complex Gaussian Fourier coefficients.
Also declared: ComparatorChallenges/DefocusingNLS.lean:46 (same declaration text).
```
noncomputable def fourierGaussianLaw : Measure (frequencyLattice → ℂ) :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice
instance OAI.DefocusingNLS.(instance at line 26) line 26
theorem OAI.DefocusingNLS.fourierGaussianLaw_map_eval line 31
Source documentation
Every coordinate has the standard complex Gaussian law.
```
theorem fourierGaussianLaw_map_eval (n : frequencyLattice) :
    fourierGaussianLaw.map (fun g => g n) = complexGaussian (1 / 2) :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.complexGaussian
theorem OAI.DefocusingNLS.fourierGaussian_coordinate_second_moment line 35
def OAI.DefocusingNLS.sobolevVariance line 43
Source documentation
The deterministic expected energy weight.
Also declared: ComparatorChallenges/DefocusingNLS.lean:49 (same declaration text).
```
noncomputable def sobolevVariance (k α : ℝ) (n : frequencyLattice) : ℝ :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice
theorem OAI.DefocusingNLS.sobolevVariance_nonneg line 46
theorem OAI.DefocusingNLS.ae_summable_gaussian_sobolev_energy line 51
Source documentation
Almost-sure finite weighted Fourier energy.
```
theorem ae_summable_gaussian_sobolev_energy (k α : ℝ) (hα : k + 6 < α) :
    ∀ᵐ g ∂fourierGaussianLaw,
      Summable (fun n => sobolevVariance k α n * Complex.normSq (g n)) := by
…
```
Mentions: OAI.DefocusingNLS.fourierGaussianLaw, OAI.DefocusingNLS.sobolevVariance
def OAI.DefocusingNLS.weightedGaussianCoefficient line 70
Source documentation
The normalized H^k coefficients, represented as an ℓ² sequence.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:52 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.weightedGaussianCoefficient@path.
```
noncomputable def weightedGaussianCoefficient (k α : ℝ)
    (g : frequencyLattice → ℂ) (n : frequencyLattice) : ℂ :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice

theorem OAI.DefocusingNLS.weightedGaussianCoefficient_eq_rpow line 75

Source documentation

These are exactly the ⟨n⟩^(k-α)-weighted coordinates of the manuscript.

theorem weightedGaussianCoefficient_eq_rpow (k α : ℝ)
    (g : frequencyLattice → ℂ) (n : frequencyLattice) :
    weightedGaussianCoefficient k α g n =
      (1 + ‖n‖ ^ 2) ^ ((k - α) / 2) • g n := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice

theorem OAI.DefocusingNLS.weightedGaussianCoefficient_norm_sq line 84
theorem OAI.DefocusingNLS.ae_mem_l2_gaussian_coefficients line 93
Source documentation
The weighted coefficient sequence lies in ℓ² almost surely.
```
theorem ae_mem_l2_gaussian_coefficients (k α : ℝ) (hα : k + 6 < α) :
    ∀ᵐ g ∂fourierGaussianLaw, Memℓp (weightedGaussianCoefficient k α g) 2 := by
…
```
Mentions: OAI.DefocusingNLS.fourierGaussianLaw