GaussianBlocks.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Independent finite heads and infinite tails

The restrictions of a product sample to disjoint index sets are independent. For complex Gaussian coordinates, every nonempty open weighted finite-head event has positive probability. These facts apply to any countable Fourier indexing, including the twelve-dimensional frequency lattice.

theorem OAI.DefocusingNLS.independent_product_restrictions line 22

Source documentation

Product coordinates on disjoint sets remain independent as entire vectors, including when one of the index sets is infinite.

theorem independent_product_restrictions {ι X : Type*} [MeasurableSpace X]
    (μ : ι → Measure X) [∀ i, IsProbabilityMeasure (μ i)]
    (S T : Set ι) (hST : Disjoint S T) :
    IndepFun S.domRestrict T.domRestrict (Measure.infinitePi μ) := by
…

theorem OAI.DefocusingNLS.independent_product_head_tail line 39

Source documentation

In particular, a finite head and its full complementary tail are independent.

theorem independent_product_head_tail {ι X : Type*} [MeasurableSpace X]
    (μ : ι → Measure X) [∀ i, IsProbabilityMeasure (μ i)] (S : Finset ι) :
    IndepFun S.restrict (Set.compl (S : Set ι)).domRestrict
      (Measure.infinitePi μ) := by
…

theorem OAI.DefocusingNLS.weighted_gaussian_head_law line 46

Source documentation

Law of a nonzero weighted finite head of an infinite Gaussian sample.

theorem weighted_gaussian_head_law {ι : Type*} (S : Finset ι)
    (v : ℝ≥0) (w : S → ℂ) :
    (Measure.infinitePi (fun _ : ι => complexGaussian v)).map
      (fun z : ι → ℂ => fun i : S => w i * z i) =
    (Measure.pi (fun _ : S => complexGaussian v)).map
      (fun z : S → ℂ => fun i => w i * z i) := by
…

Mentions: OAI.DefocusingNLS.complexGaussian

theorem OAI.DefocusingNLS.weighted_gaussian_head_open_pos line 60

Source documentation

Positive probability of every prescribed open finite-head neighborhood.

theorem weighted_gaussian_head_open_pos {ι : Type*} (S : Finset ι)
    {v : ℝ≥0} (hv : v ≠ 0) (w : S → ℂ) (hw : ∀ i, w i ≠ 0)
    (U : Set (S → ℂ)) (hU : IsOpen U) (hne : U.Nonempty) :
    0 < Measure.infinitePi (fun _ : ι => complexGaussian v)
      ((fun z : ι → ℂ => fun i : S => w i * z i) ⁻¹' U) := by
…

Mentions: OAI.DefocusingNLS.complexGaussian