FiniteGaussian.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Positivity of finite Gaussian Fourier blocks

A finite list of independent nondegenerate complex Gaussians charges every nonempty open coefficient set. Multiplication by any nonzero Fourier weights preserves that property. This is the finite-block ingredient in the Gaussian support argument for Corollary 1.2 of the stable defocusing NLS manuscript.

theorem OAI.DefocusingNLS.gaussianReal_isOpenPosMeasure line 23
Source documentation
A nondegenerate real Gaussian is positive on nonempty open sets.
```
theorem gaussianReal_isOpenPosMeasure (m : ℝ) {v : ℝ≥0} (hv : v ≠ 0) :
    (gaussianReal m v).IsOpenPosMeasure :=
…
```
def OAI.DefocusingNLS.complexGaussian line 29
Source documentation
Independent centered real and imaginary Gaussian coordinates, each of variance v. The usual standard complex Gaussian takes v = 1/2.
Also declared: ComparatorChallenges/DefocusingNLS.lean:35 (same declaration text).
```
noncomputable def complexGaussian (v : ℝ≥0) : Measure ℂ :=
…
```
instance OAI.DefocusingNLS.complexGaussian_isProbabilityMeasure line 33
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:39 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.complexGaussian_isProbabilityMeasure@path.
theorem OAI.DefocusingNLS.complexGaussian_isOpenPosMeasure line 39
Source documentation
Real and imaginary nondegeneracy give full topological support on ℂ.
```
theorem complexGaussian_isOpenPosMeasure {v : ℝ≥0} (hv : v ≠ 0) :
    (complexGaussian v).IsOpenPosMeasure := by
…
```
Mentions: OAI.DefocusingNLS.complexGaussian
theorem OAI.DefocusingNLS.finite_complexGaussian_isOpenPosMeasure line 46
Source documentation
The independent finite Fourier block has full support.
```
theorem finite_complexGaussian_isOpenPosMeasure {ι : Type*} [Fintype ι]
    {v : ℝ≥0} (hv : v ≠ 0) :
    (Measure.pi (fun _ : ι => complexGaussian v)).IsOpenPosMeasure := by
…
```
Mentions: OAI.DefocusingNLS.complexGaussian

theorem OAI.DefocusingNLS.weighted_finite_complexGaussian_isOpenPosMeasure line 54

Source documentation

Multiplying each finite Fourier coefficient by a nonzero weight preserves full support. In particular all polynomial Fourier-decay weights qualify.

theorem weighted_finite_complexGaussian_isOpenPosMeasure
    {ι : Type*} [Fintype ι] {v : ℝ≥0} (hv : v ≠ 0)
    (w : ι → ℂ) (hw : ∀ i, w i ≠ 0) :
    ((Measure.pi (fun _ : ι => complexGaussian v)).map
      (fun z : ι → ℂ => fun i => w i * z i)).IsOpenPosMeasure := by
…

Mentions: OAI.DefocusingNLS.complexGaussian

theorem OAI.DefocusingNLS.weighted_finite_complexGaussian_ball_pos line 70

Source documentation

Every prescribed finite coefficient vector can be approximated with positive probability, including after nonzero Fourier weights are applied.

theorem weighted_finite_complexGaussian_ball_pos
    {ι : Type*} [Fintype ι] {v : ℝ≥0} (hv : v ≠ 0)
    (w : ι → ℂ) (hw : ∀ i, w i ≠ 0) (f : ι → ℂ) {r : ℝ} (hr : 0 < r) :
    0 < ((Measure.pi (fun _ : ι => complexGaussian v)).map
      (fun z : ι → ℂ => fun i => w i * z i)) (Metric.ball f r) := by
…

Mentions: OAI.DefocusingNLS.complexGaussian