For any probability measure \(\mu \) on \(\Omega \), any random matrix \(A\), and any \(\varepsilon \in \mathbb {R}\),

The bad event at \(x=0\) is always empty because \(\varepsilon \cdot 0 \lt |0-0|\) simplifies to \(0 \lt 0\), which is false.

Let \(X : \Omega \to \mathbb {R}\) be measurable with \(X_*\mu = N(0,\sigma _0)\). Then for any constant \(c\in \mathbb {R}\),

This is an auxiliary restatement of gaussianReal_map_const_mul phrased for easy application in the inductive step of sum_scaled_iid_gaussian_map.

Let \(Y_j : \Omega \to \mathbb {R}\) be i.i.d. with law \(N(0,\sigma _0)\), and let \(x : \iota \to \mathbb {R}\) be a fixed coefficient vector. For any finite set \(s\),

The proof proceeds by induction on the finset \(s\), using independence and map_const_mul_gaussian at each step.

If the row vectors of \(A\) (as \((\mathrm{Fin}\, d\to \mathbb {R})\)-valued random variables) are mutually independent under \(\mu \), then for any fixed \(x\in \mathbb {R}^d\) the scalar row-projections \((A\, \omega ).\texttt{toEuclideanLin}\, x\, i = \sum _j A_{\omega ,i,j}\, x_j\) are independent across \(i\in \mathrm{Fin}\, k\), since each is a measurable function of a distinct row of \(A\).

For a matrix \(A\in \mathbb {R}^{k\times d}\), a vector \(x\in \mathbb {R}^d\), and an index \(i\in \mathrm{Fin}\, k\),

This definitional equality unfolds the linear map into its explicit sum form.

For a matrix \(A\) and vector \(x\),

This expresses the squared Euclidean norm of \(Ax\) as the sum of the squares of its coordinates.

The function \(h(u) = u^2 + u + \log (1-u)\) has derivative \(h'(u) = u(1-2u)/(1-u)\) at every \(u \lt 1\). This derivative identity is the key ingredient in the monotonicity argument used to bound the centered chi-squared log-MGF.

The evaluation \(0^2 + 0 + \log (1-0) = 0\) establishes the base case for the Taylor bound, confirming that \(h(0)=0\) in the derivative argument for neg_log_one_sub_two_mul_le_two_sq.

For every \(s\in \mathbb {R}\) with \(|s|\le 1/4\),

This inequality is the Taylor-based analytic core of the centered chi-squared MGF bound; it is proved by showing that the auxiliary function \(h(u)=u^2+u+\log (1-u)\) satisfies \(h(0)=0\) and has non-negative derivative on \([0,1/2]\) and non-positive derivative on \([-1/2,0]\).

For \(Z\sim N(0,1)\) and \(2s\lt 1\),

This is the closed-form moment-generating function of the standard chi-squared distribution.

For \(Y\sim N(0,v)\) with \(v\ne 0\) and \(2tv \lt 1\),

This generalizes integral_exp_mul_sq_standardGaussian from unit variance to an arbitrary non-zero NNReal variance \(v\).

For \(v\ne 0\) and \(2tv \lt 1\), the function \(y\mapsto e^{t y^2}\) is integrable with respect to \(N(0,v)\). This integrability statement accompanies integral_exp_mul_sq_gaussianReal_zero and is a prerequisite for the Fubini and interchange-of-expectation arguments in centered_chi_squared_step.

Let \(Y_1,\dots ,Y_k:\Omega \to \mathbb {R}\) be i.i.d. with law \(N(0,1/k)\) under a probability measure \(\mu \), and let \(0\lt \varepsilon \lt 1\). Then

The proof applies the Bernstein tail bound to the i.i.d. sum of centered chi-squared summands, using hasBernsteinMGF_centered_chi_squared and the generic sum and tail-bound lemmas from the Bernstein framework.