The Gaussian embedding into L² and its clipping error

On a finite-dimensional real inner product space E, the random linear observable y ↦ ⟪x, y⟫ under the standard Gaussian measure has variance ‖x‖² and fourth moment 3 ‖x‖⁴. Consequently these observables define a linear isometry from E into L²(stdGaussian E).

Clipping the observable at height M > 0 gives a bounded L² function whose squared error is at most 3 ‖x‖⁴ / (16 M²). For vectors in the unit ball this is the 3 / (16 M²) estimate, or the norm bound √3 / (4 M), used in the Gaussian truncation proof of Grothendieck's inequality. The construction also works in dimension zero.

We use Mathlib's basis-independent ProbabilityTheory.stdGaussian, IsGaussian.memLp_dual, and the real Gaussian even-moment formula, rather than introducing a second finite Gaussian probability space.

References

• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, §8.1.

theorem TauCeti.Probability.memLp_inner_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x : E) (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp (fun (y : E) => inner ℝ x y) p (ProbabilityTheory.stdGaussian E)

A standard Gaussian linear observable belongs to every finite Lᵖ space.

theorem TauCeti.Probability.integral_pow_two_mul_inner_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x : E) (n : ℕ) : ∫ (y : E), inner ℝ x y ^ (2 * n) ∂ProbabilityTheory.stdGaussian E = ‖x‖ ^ (2 * n) * ↑(2 * n - 1).doubleFactorial

The even moments of a standard Gaussian linear observable.

theorem TauCeti.Probability.integral_sq_inner_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x : E) : ∫ (y : E), inner ℝ x y ^ 2 ∂ProbabilityTheory.stdGaussian E = ‖x‖ ^ 2

The second moment of a standard Gaussian linear observable.

theorem TauCeti.Probability.integral_pow_four_inner_stdGaussian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x : E) : ∫ (y : E), inner ℝ x y ^ 4 ∂ProbabilityTheory.stdGaussian E = 3 * ‖x‖ ^ 4

The fourth moment of a standard Gaussian linear observable.

noncomputable def TauCeti.Probability.gaussianL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : E →ₗᵢ[ℝ] ↥(MeasureTheory.Lp ℝ 2 (ProbabilityTheory.stdGaussian E))

A finite-dimensional real inner product space embeds isometrically into Gaussian L² by sending a vector to its random linear observable.

theorem TauCeti.Probability.gaussianL2_ae_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x : E) : ↑↑(gaussianL2 x) =ᵐ[ProbabilityTheory.stdGaussian E] fun (y : E) => inner ℝ x y

A representative of the canonical Gaussian L² observable.

noncomputable def TauCeti.Probability.clippedGaussianL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x : E) (M : ℝ) : ↥(MeasureTheory.Lp ℝ 2 (ProbabilityTheory.stdGaussian E))

A Gaussian observable clipped to [-M, M] for M ≥ 0, as an element of L². For negative M, the max-min formula gives the constant -M.

theorem TauCeti.Probability.clippedGaussianL2_ae_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x : E) (M : ℝ) : ↑↑(clippedGaussianL2 x M) =ᵐ[ProbabilityTheory.stdGaussian E] fun (y : E) => max (-M) (min M (inner ℝ x y))

A bounded representative of the clipped Gaussian observable.

theorem TauCeti.Probability.ae_abs_clippedGaussianL2_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x : E) (M : ℝ) (hM : 0 ≤ M) : ∀ᵐ (y : E) ∂ProbabilityTheory.stdGaussian E, |↑↑(clippedGaussianL2 x M) y| ≤ M

The clipped observable is almost everywhere bounded by its clipping height.

theorem TauCeti.Probability.norm_clippedGaussianL2_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x : E) (M : ℝ) (hM : 0 ≤ M) : ‖clippedGaussianL2 x M‖ ≤ ‖x‖

Clipping does not increase the L² norm of the Gaussian observable.

theorem TauCeti.Probability.norm_sub_clippedGaussianL2_sq_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (x : E) {M : ℝ} (hM : 0 < M) : ‖gaussianL2 x - clippedGaussianL2 x M‖ ^ 2 ≤ 3 * ‖x‖ ^ 4 / (16 * M ^ 2)

Clipping a Gaussian linear observable has squared L² error at most 3 ‖x‖⁴ / (16 M²).

theorem TauCeti.Probability.norm_sub_clippedGaussianL2_sq_le_of_norm_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {x : E} (hx : ‖x‖ ≤ 1) {M : ℝ} (hM : 0 < M) : ‖gaussianL2 x - clippedGaussianL2 x M‖ ^ 2 ≤ 3 / (16 * M ^ 2)

The uniform clipping-error bound for Gaussian observables of unit-ball vectors.

theorem TauCeti.Probability.norm_sub_clippedGaussianL2_le_of_norm_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {x : E} (hx : ‖x‖ ≤ 1) {M : ℝ} (hM : 0 < M) : ‖gaussianL2 x - clippedGaussianL2 x M‖ ≤ √3 / (4 * M)

The clipping error of the Gaussian observable of a unit-ball vector has L² norm at most √3 / (4 * M).