GaussianRealization.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

A measurable Hilbert-valued realization of the Fourier series

The weighted coefficients are realized in the standard ℓ² Hilbert model of the Sobolev norm. The realization is a measurable sum of coordinate vectors, and agrees almost surely with the prescribed coefficients.

abbrev OAI.DefocusingNLS.FourierL2 line 22
Also declared: ComparatorChallenges/DefocusingNLS.lean:58 (same declaration text).
instance OAI.DefocusingNLS.(instance at line 26) line 26
Source documentation
Finite coordinate vectors have dense complex span, so this Hilbert model is separable.
```
instance : SeparableSpace FourierL2 := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2
instance OAI.DefocusingNLS.(instance at line 46) line 46
instance OAI.DefocusingNLS.(instance at line 47) line 47
def OAI.DefocusingNLS.weightedGaussianVector line 50
Source documentation
Measurable Hilbert-valued sum of the weighted Gaussian coordinates.
Also declared: ComparatorChallenges/DefocusingNLS.lean:63 (same declaration text).
```
noncomputable def weightedGaussianVector (k α : ℝ)
    (g : frequencyLattice → ℂ) : FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.measurable_weightedGaussianVector line 54
theorem OAI.DefocusingNLS.ae_weightedGaussianVector_coefficients line 64
Source documentation
In the summable range, the measurable realization has precisely the prescribed Fourier coefficients almost surely.
```
theorem ae_weightedGaussianVector_coefficients (k α : ℝ) (hα : k + 6 < α) :
    ∀ᵐ g ∂fourierGaussianLaw, ∀ n,
      weightedGaussianVector k α g n = weightedGaussianCoefficient k α g n := by
…
```
Mentions: OAI.DefocusingNLS.fourierGaussianLaw, OAI.DefocusingNLS.weightedGaussianVector
def OAI.DefocusingNLS.sobolevFourierCoefficient line 74
Source documentation
The unweighted Fourier coefficient of an element of the H^k model.
Also declared: ComparatorChallenges/DefocusingNLS.lean:67 (same declaration text).
```
noncomputable def sobolevFourierCoefficient (k : ℝ) (f : FourierL2)
    (n : frequencyLattice) : ℂ :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.frequencyLattice
theorem OAI.DefocusingNLS.ae_sobolevFourierCoefficient line 79
Source documentation
Undoing the Sobolev weight gives exactly gₙ / ⟨n⟩^α.
```
theorem ae_sobolevFourierCoefficient (k α : ℝ) (hα : k + 6 < α) :
    ∀ᵐ g ∂fourierGaussianLaw, ∀ n,
      sobolevFourierCoefficient k (weightedGaussianVector k α g) n =
        (1 + ‖n‖ ^ 2) ^ (-α / 2) • g n := by
…
```
Mentions: OAI.DefocusingNLS.fourierGaussianLaw, OAI.DefocusingNLS.sobolevFourierCoefficient, OAI.DefocusingNLS.weightedGaussianVector
def OAI.DefocusingNLS.weightedGaussianLaw line 91
Source documentation
The corresponding probability law in the Hilbert model.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:71 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.weightedGaussianLaw@path.
```
noncomputable def weightedGaussianLaw (k α : ℝ) : Measure FourierL2 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2
instance OAI.DefocusingNLS.(instance at line 94) line 94