GaussianMoments.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Second moments of the complex Fourier coefficients

The complex Gaussian used for finite Fourier blocks has second moment twice the variance of one real coordinate. This includes the zero-variance case.

theorem OAI.DefocusingNLS.real_gaussian_second_moment line 19
Source documentation
The nonnegative second moment of a centered real Gaussian.
```
theorem real_gaussian_second_moment (v : ℝ≥0) :
    (∫⁻ x : ℝ, ENNReal.ofReal (x ^ 2) ∂gaussianReal 0 v) = v := by
…
```
theorem OAI.DefocusingNLS.complex_gaussian_second_moment line 27
Source documentation
A complex coefficient with independent real/imaginary variance v has squared-modulus expectation 2*v.
```
theorem complex_gaussian_second_moment (v : ℝ≥0) :
    (∫⁻ z : ℂ, ENNReal.ofReal (‖z‖ ^ 2) ∂complexGaussian v) = 2 * v := by
…
```
Mentions: OAI.DefocusingNLS.complexGaussian
theorem OAI.DefocusingNLS.standard_complex_gaussian_normSq_moment line 40
Source documentation
The standard complex Gaussian has unit squared-modulus expectation.
```
theorem standard_complex_gaussian_normSq_moment :
    (∫⁻ z : ℂ, ENNReal.ofReal (Complex.normSq z) ∂complexGaussian (1 / 2)) = 1 := by
…
```
Mentions: OAI.DefocusingNLS.complexGaussian