Sharp standard Gaussian concentration for every Lipschitz observable

Mathematical statement

For every globally L-Lipschitz scalar observable on the stated finite real Hilbert/Borel space, its actual standard Gaussian centered exponential integral is at most exp(L^2*t^2/2) for every signed real t. Actual first moments and all exponential domains are produced by the existing shared domain theorem; the C1 restriction used inside the proof is removed internally.

theorem integral_exp_centered_le_stdGaussian_of_lipschitz
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {L : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith L f) (t : ℝ) :
    (∫ x, Real.exp (t * (f x - ∫ z, f z ∂ProbabilityTheory.stdGaussian E))
      ∂ProbabilityTheory.stdGaussian E) ≤ Real.exp ((L : ℝ)^2 * t^2 / 2)

Proof roadmap

1. 1Establish the actual Gaussian domains

   The existing Fernique-domain declaration proves first Bochner integrability and every signed centered exponential L1 from global Lipschitz growth. Shifting the center gives radial exponential domains. Polynomial factors are dominated by a larger radial exponential, also on the actual product Gaussian equipped with its Banach max norm.

2. 2Derive Gaussian Stein integration by parts

   For the temporary C1 case, the canonical ASTIS Gaussian density with respect to the given Hilbert volume has derivative -w(x) inner(x,-). Growth, the genuine Gaussian second moment and the derivative bound by L prove every Haar integration-by-parts integrability input. The resulting Stein equality has no supplied domain certificate.

3. 3Rotate two independent standard Gaussians

   For X,Y independently distributed as gamma, U=cos(theta)X+sin(theta)Y and W=-sin(theta)X+cos(theta)Y have the same product law. Differentiate F(theta)=E[f(X) exp(t(f(U)-m))] using an explicit polynomial times radial-exponential domination valid for every theta. The inverse relation X=cos(theta)U-sin(theta)W is exact.

4. 4Apply Stein only to the affine Lipschitz factor

   After rotation, fix U=u and let a(u) be the Riesz representative of Df(u). Apply Stein in W to the C1 Lipschitz function W→f(cu-sW). Its derivative is -s Df(cu-sW). The exponential is constant in this conditional variable; it is never asserted globally Lipschitz. Actual product L1 and Fubini justify the conditional calculation.

5. 5Recover the covariance bound with correct sign

   The inner integral has absolute value at most L squared. On theta in [0,pi/2] and t≥0 the factor -sin(theta)t is nonpositive, so the upper bound on the inner integral gives a lower bound on F prime. For C=t L squared M, H=F-cos(theta)C is nondecreasing by the mean-value theorem. Actual derivative existence gives endpoint continuity. Endpoint independence yields the covariance inequality.

6. 6Prove the sharp Herbst estimate and both signs

   All signed exponential domains give integrableExpSet=the full real line. Pinned Mathlib MGF differentiation gives the actual M prime. The covariance estimate implies M prime≤t L squared M on t≥0. The integrating factor exp(-L squared t squared/2)M is nonincreasing and equals one at zero. Apply the result to -f and -t for negative parameters.

7. 7Smooth internally without changing the constant

   Use the actual nonnegative normalized compactly supported smooth bump against canonical Hilbert volume. Its outer radius is epsilon_n=2^-n and its mass is one. The convolution f_n is C1 and remains globally L Lipschitz. The uniform error is at most L epsilon_n. This introduces no differentiability assumption on the public observable.

8. 8Pass the actual center and exponential integral to the limit

   First-moment integrability and the uniform approximation give |m_n-m|≤L epsilon_n. The centered exponents converge pointwise, and every n is dominated by exp(2|t|L) exp(t(f-m)), whose L1 was proved before the sharp estimate. Dominated convergence passes the same sharp bound to f. Zero L and the zero-dimensional carrier are discharged directly as constant observables.