Projections of the standard Gaussian measure

Let X be a standard Gaussian vector of a finite-dimensional real inner product space E (stdGaussian E). Its covariance is the inner product, so:

• the projection ⟪u, X⟫ is a centered Gaussian of variance ‖u‖ ^ 2 (stdGaussian_map_inner);
• projections onto orthogonal vectors are uncorrelated, and since they are jointly Gaussian, independent (indepFun_inner_stdGaussian), so their joint law is the product of their laws (stdGaussian_map_inner_prod).

Hence the projection onto a nonzero u lands in a set s with probability at most volume s / (√(2π) ‖u‖) (stdGaussian_inner_mem_le), and has absolute value at least c > 0 with probability at most ‖u‖ ^ 2 / c ^ 2 (stdGaussian_le_abs_inner_le).

The standard Gaussian vector of EuclideanSpace ℝ ι is a vector of independent standard Gaussian coordinates (measurePreserving_toLp_pi_gaussianReal), which transfers these facts to the product measure Measure.pi fun _ : ι => gaussianReal 0 1 on ι → ℝ.

Main results

• ProbabilityTheory.stdGaussian_map_inner: the law of a projection.
• ProbabilityTheory.indepFun_inner_stdGaussian: projections onto orthogonal vectors are independent.
• ProbabilityTheory.stdGaussian_map_inner_prod: the joint law of projections onto orthogonal vectors.
• ProbabilityTheory.stdGaussian_inner_mem_le, ProbabilityTheory.stdGaussian_le_abs_inner_le: window and tail bounds for a projection.
• ProbabilityTheory.measurePreserving_toLp_pi_gaussianReal: independent standard Gaussian coordinates form a standard Gaussian vector of EuclideanSpace ℝ ι.

theorem ProbabilityTheory.stdGaussian_map_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (u : E) : MeasureTheory.Measure.map (fun (x : E) => inner ℝ u x) (stdGaussian E) = gaussianReal 0 (‖u‖₊ ^ 2)

The law of a projection. Under the standard Gaussian measure, ⟪u, ·⟫ is a centered Gaussian of variance ‖u‖ ^ 2.

theorem ProbabilityTheory.indepFun_inner_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u v : E} (huv : inner ℝ u v = 0) : IndepFun (fun (x : E) => inner ℝ u x) (fun (x : E) => inner ℝ v x) (stdGaussian E)

Orthogonal projections are independent. Under the standard Gaussian measure, ⟪u, ·⟫ and ⟪v, ·⟫ are jointly Gaussian with covariance ⟪u, v⟫, so they are independent when u and v are orthogonal.

theorem ProbabilityTheory.stdGaussian_map_inner_prod {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u v : E} (huv : inner ℝ u v = 0) : MeasureTheory.Measure.map (fun (x : E) => (inner ℝ u x, inner ℝ v x)) (stdGaussian E) = (gaussianReal 0 (‖u‖₊ ^ 2)).prod (gaussianReal 0 (‖v‖₊ ^ 2))

The joint law of the projections onto orthogonal vectors u and v is the product of centered Gaussians of variances ‖u‖ ^ 2 and ‖v‖ ^ 2.

theorem ProbabilityTheory.stdGaussian_inner_mem_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u : E} (hu : u ≠ 0) {s : Set ℝ} (hs : MeasurableSet s) : (stdGaussian E) {x : E | inner ℝ u x ∈ s} ≤ ENNReal.ofReal (√(2 * Real.pi) * ‖u‖)⁻¹ * MeasureTheory.volume s

Window bound. The projection of a standard Gaussian vector onto a nonzero vector u lands in a measurable set s with probability at most volume s / (√(2π) ‖u‖).

theorem ProbabilityTheory.stdGaussian_le_abs_inner_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (u : E) {c : ℝ} (hc : 0 < c) : (stdGaussian E) {x : E | c ≤ |inner ℝ u x|} ≤ ENNReal.ofReal (‖u‖ ^ 2 / c ^ 2)

Tail bound. The projection of a standard Gaussian vector onto u has absolute value at least c > 0 with probability at most ‖u‖ ^ 2 / c ^ 2.

theorem ProbabilityTheory.measurePreserving_toLp_pi_gaussianReal (ι : Type u_2) [Fintype ι] : MeasureTheory.MeasurePreserving (WithLp.toLp 2) (MeasureTheory.Measure.pi fun (x : ι) => gaussianReal 0 1) (stdGaussian (EuclideanSpace ℝ ι))

Independent standard Gaussian coordinates form a standard Gaussian vector of EuclideanSpace ℝ ι.