GaussianFullSupport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Full support of the Fourier Gaussian law

The small-tail/independent-head estimate is converted to positive mass of all Hilbert balls, and hence all nonempty open Sobolev sets.

lemma OAI.DefocusingNLS.ofReal_norm_sub_sq_le line 18
lemma OAI.DefocusingNLS.sqrt_weight_norm_sq line 32

theorem OAI.DefocusingNLS.gaussian_error_energy_pos line 43

Source documentation

All squared-error balls about square-summable coefficient vectors have positive probability under a positive square-summable Gaussian weighting.

theorem gaussian_error_energy_pos (w : ι → ℝ) (hw : ∀ i, 0 < w i)
    (hwsum : Summable w) (f : ι → ℂ) (hfsum : Summable (fun i => ‖f i‖ ^ 2))
    {r : ℝ} (hr : 0 < r) :
    0 < Measure.infinitePi (fun _ : ι => complexGaussian (1 / 2))
      {g | (∑' i, ENNReal.ofReal (‖(Real.sqrt (w i) : ℂ) * g i - f i‖ ^ 2)) <
        ENNReal.ofReal r} := by
…

Mentions: OAI.DefocusingNLS.complexGaussian

theorem OAI.DefocusingNLS.weightedGaussianLaw_ball_pos line 101
Source documentation
Every Hilbert ball has positive probability for the Gaussian Fourier law at exactly the manuscript's Sobolev threshold.
```
theorem weightedGaussianLaw_ball_pos (k α : ℝ) (hα : k + 6 < α)
    (f : FourierL2) {r : ℝ} (hr : 0 < r) :
    0 < weightedGaussianLaw k α (Metric.ball f r) := by
…
```
Mentions: OAI.DefocusingNLS.FourierL2
theorem OAI.DefocusingNLS.weightedGaussianLaw_isOpenPosMeasure line 138
Source documentation
The Fourier Gaussian law has full support in its Sobolev Hilbert model.
```
theorem weightedGaussianLaw_isOpenPosMeasure (k α : ℝ) (hα : k + 6 < α) :
    (weightedGaussianLaw k α).IsOpenPosMeasure := by
…
```