GaussianSmallBalls.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Small balls for square-summable Gaussian coefficients

The random tail has arbitrarily small expected energy; a finite head can be placed near any prescribed target independently of that tail. The argument proves the coefficient-space probability estimate used for Hilbert support.

def OAI.DefocusingNLS.gaussianTailEnergy line 26
Source documentation
Energy beyond a finite set of Fourier frequencies.
```
noncomputable def gaussianTailEnergy (w : ι → ℝ) (S : Finset ι) (g : ι → ℂ) : ℝ≥0∞ :=
…
```
theorem OAI.DefocusingNLS.measurable_gaussianTailEnergy line 29

theorem OAI.DefocusingNLS.gaussianTailEnergy_mean line 36

Source documentation

The mean tail energy is exactly the sum of the tail variances.

theorem gaussianTailEnergy_mean (w : ι → ℝ) (S : Finset ι) :
    (∫⁻ g, gaussianTailEnergy w S g
      ∂Measure.infinitePi (fun _ : ι => complexGaussian (1 / 2))) =
    ∑' i : ↥((S : Set ι)ᶜ), ENNReal.ofReal (w i) := by
…

Mentions: OAI.DefocusingNLS.gaussianTailEnergy, OAI.DefocusingNLS.complexGaussian

theorem OAI.DefocusingNLS.gaussianTailEnergy_small_pos line 58

Source documentation

A small expected tail produces a positive-probability small-tail event.

theorem gaussianTailEnergy_small_pos (w : ι → ℝ) (S : Finset ι) {c : ℝ≥0∞}
    (hmean : (∑' i : ↥((S : Set ι)ᶜ), ENNReal.ofReal (w i)) < c) :
    0 < Measure.infinitePi (fun _ : ι => complexGaussian (1 / 2))
      {g | gaussianTailEnergy w S g < c} := by
…

Mentions: OAI.DefocusingNLS.complexGaussian, OAI.DefocusingNLS.gaussianTailEnergy

theorem OAI.DefocusingNLS.exists_small_variance_target_tails line 68

Source documentation

One finite set makes both a summable variance tail and a square-summable fixed target tail small.

theorem exists_small_variance_target_tails (w : ι → ℝ) (hw : Summable w)
    (f : ι → ℂ) (hf : Summable (fun i => ‖f i‖ ^ 2)) {c : ℝ≥0∞} (hc : 0 < c) :
    ∃ S : Finset ι,
      (∑' i : ↥((S : Set ι)ᶜ), ENNReal.ofReal (w i)) < c ∧
      (∑' i : ↥((S : Set ι)ᶜ), ENNReal.ofReal (‖f i‖ ^ 2)) < c := by
…

theorem OAI.DefocusingNLS.gaussian_head_and_tail_pos line 80

Source documentation

A finite prescribed coefficient error and a small infinite-tail energy occur together with positive probability.

theorem gaussian_head_and_tail_pos (w : ι → ℝ) (hw : ∀ i, 0 < w i)
    (S : Finset ι) (f : ι → ℂ) {δ : ℝ} (hδ : 0 < δ) {c : ℝ≥0∞}
    (hmean : (∑' i : ↥((S : Set ι)ᶜ), ENNReal.ofReal (w i)) < c) :
    0 < Measure.infinitePi (fun _ : ι => complexGaussian (1 / 2))
      ({g | (∑ i : S, ‖(Real.sqrt (w i) : ℂ) * g i - f i‖ ^ 2) < δ} ∩
        {g | gaussianTailEnergy w S g < c}) := by
…

Mentions: OAI.DefocusingNLS.complexGaussian, OAI.DefocusingNLS.gaussianTailEnergy