LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Gaussian anchored bounded sums have uniform cumulant and Fourier bounds

Statement

Assume AC. Fix $0 < γ \leq 1$ . Let $1 \leq d \leq 4$ , $s > 0$ , $B > 0$ , and let $X_{1}, \dots, X_{m}, Z$ be independent centered random vectors in $R^{d}$ , where $m \geq 0$ , $∣ X_{j} ∣ \leq B$ almost surely, and $Z \sim N_{d} (0, G)$ . Suppose $S = Z + \sum_{j} X_{j}$ has covariance $s I_{d}$ and $G \geq γ s I_{d}$ in quadratic form order. There is an absolute constant $C_{0} \geq 1$ such that, with $τ = C_{0} B$ , the logarithmic moment generating function $K (z) = \log E e^{z \cdot S}, K (0) = 0,$ has a single analytic branch on the complex Euclidean ball $τ ∣ z ∣ < 1$ , and $∣ \partial_{u} \partial_{v}^{2} K (z) ∣ \leq τ s ∣ u ∣ ∣ v ∣^{2} (u, v \in R^{d}, τ ∣ z ∣ < 1) .$ Here $z \cdot S$ uses the complex bilinear dot product and $∣ z ∣^{2} = \sum_{i} ∣ z_{i} ∣^{2}$ . Every real exponential tilt $P_{h} (d ω) = e^{h \cdot S - K (h)} P (d ω)$ is defined, and its characteristic function satisfies $∣ φ_{h} (t) ∣ : = ∣ E_{h} e^{i t \cdot S} ∣ \leq e^{- γ s ∣ t ∣^{2} / 2} (t, h \in R^{d}),$ where $K (h) = \log E e^{h \cdot S}$ for real $h$ , also outside the analytic ball. Put $κ = τ / \sqrt{s}$ . For every fixed $a > 0$ and integer $N \geq 1$ there is a finite $C_{a, N, γ}$ , uniform in $1 \leq d \leq 4$ , such that, if $0 < κ \leq 1$ , $(2 π)^{- d} \int_{∣ t ∣ \geq a / τ} ∣ φ_{h} (t) ∣ d t \leq C_{a, N, γ} κ^{N} s^{- d / 2},$ $(2 π)^{- d} \int_{∣ t ∣ \geq a / τ} ∣ t \cdot v ∣ ∣ φ_{h} (t) ∣ d t \leq C_{a, N, γ} κ^{N} ∣ v ∣ s^{- (d + 1) / 2} .$ All assertions hold with the same $C_{0}$ , $B$ , $s$ , and $γ$ for $A S$ , where $A$ is any real $k \times d$ matrix with $1 \leq k \leq d$ and $A A^{T} = I_{k}$ . This includes every coordinate prefix, every orthogonal change of coordinates, and their compositions. In particular it covers the normalized joint sum and difference of two independent children by applying the assertion in their joint dimension, provided that dimension is at most four and the joint input satisfies the stated covariance assumptions.

Facts & Assumptions

Given: The hypotheses of the Statement; all vector norms are Euclidean, and all matrix orders are orders of real quadratic forms.

[F1]

Finite products of integrable functions of independent variables factor in expectation. Expectations factor over finite products of independent random variables.

[F2]

Dominated convergence interchanges limits and integrals under an integrable absolute majorant. Dominated convergence.

[F3]

Absolute Fubini and nonnegative Tonelli apply to the probability and Lebesgue integrals below. Fubini's theorem for L^1 functions on a sigma-finite product, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product.

[F4]

A positive definite Gaussian law has density $q_{G} (x) = (2 π)^{- d / 2} (\det G)^{- 1 / 2} e^{- x^{T} G^{- 1} x / 2}$ and a Gaussian with covariance $G$ has characteristic function $e^{- t^{T} G t / 2}$ . A positive-definite multivariate normal law has its Gaussian density, Characteristic function of a multivariate normal law.

[F6]

Locally uniformly convergent holomorphic series are holomorphic, the one-variable identity theorem extends equality from a real interval, and linear changes of Lebesgue variables have their determinant Jacobian. A locally uniformly convergent series of holomorphic functions may be differentiated term by term, Identity theorem for holomorphic functions, A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions.

[F5]

Euclidean Cauchy–Schwarz bounds $∣ u \cdot x ∣ \leq ∣ u ∣ ∣ x ∣$ , and its integral version follows by integrating $(f - c g)^{2} \geq 0$ and minimizing in real $c$ . Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation.

[A1]

AC is assumed and inherited by the Gaussian suppliers. The Axiom of Choice.

Proof

1.1A1givenF2F5F6

Fix one centered bounded summand $X$ with covariance $D$ , and put $M (z) = E e^{z \cdot X}$ . Its exponential series converges uniformly on every bounded complex set because $∣ X ∣ \leq B$ , and the expectation of its absolute series is bounded by $e^{B ∣ z ∣}$ ; thus termwise integration defines an entire function and its derivatives are the expectations of the corresponding polynomial factors times the exponential. Fix an absolute $b > 0$ with $e^{b} - 1 \leq 1 / 2$ . If $B ∣ z ∣ < b$ , then $∣ M (z) - 1 ∣ \leq e^{B ∣ z ∣} - 1 \leq 1 / 2$ , so the convergent power series for $\log (1 + (M (z) - 1))$ supplies a single analytic logarithm vanishing at zero.

1.2F2F4F6algebra

Completing the square in the density in [F4] shows $E e^{h \cdot Z} = e^{h^{T} G h / 2}$ for real $h$ and that its real tilt is $N_{d} (G h, G)$ . The same integral for complex $z$ converges absolutely on bounded complex sets: $e^{Re (z) \cdot x}$ times the Gaussian density is a constant times a translated Gaussian density, which dominates its polynomial derivatives on smaller bounded sets. Its exponential series or differentiated integral therefore gives an entire function, and the real identity extends to complex arguments. To justify that last extension without a several-variable identity theorem, fix all but the first coordinate real and apply the one-variable identity theorem, then successively free each remaining coordinate. Thus the Gaussian cumulant is $z^{T} G z / 2$ and has zero third derivative.

2.1step 1.1F5

On this ball, writing subscripts for directional derivatives, the bounds $∣ e^{z \cdot X} ∣ \leq e^{b}$ , $∣ u \cdot X ∣ \leq B ∣ u ∣$ , and $E (v \cdot X)^{2} = v^{T} D v$ give $∣ M_{u} ∣ \leq e^{b} B ∣ u ∣$ , $∣ M_{v} ∣ \leq e^{b} \sqrt{v^{T} D v}$ , $∣ M_{v v} ∣ \leq e^{b} v^{T} D v$ , $∣ M_{u v} ∣ \leq e^{b} B ∣ u ∣ \sqrt{v^{T} D v}$ , and $∣ M_{u v v} ∣ \leq e^{b} B ∣ u ∣ v^{T} D v$ . These inequalities also hold when $D$ is singular: a direction with zero second moment has $v \cdot X = 0$ almost surely.

2.2step 1.2F1F4

Every real tilt exists because all bounded-summand moment generating functions and the Gaussian one are finite and strictly positive. Its density with respect to the original independent joint law factors as the product of the separately normalized tilt densities. Hence those summands remain independent under the tilt. Step 1.2 shows that the Gaussian factor retains covariance $G$ , while each other factor has a characteristic function of modulus at most one because $∣ e^{i t \cdot X_{j}} ∣ = 1$ . Factorization and [F4] therefore give $∣ φ_{h} (t) ∣ \leq e^{- t^{T} G t / 2} \leq e^{- γ s ∣ t ∣^{2} / 2}$ for every real $h, t$ .

3.1step 1.1step 2.1algebrachoose

Direct differentiation gives $(\log M)_{u v v} = M_{u v v} / M - (M_{u} M_{v v} + 2 M_{v} M_{u v}) / M^{2} + 2 M_{u} M_{v}^{2} / M^{3}$ . Since $∣ M ∣ \geq 1 / 2$ , step 2.1 bounds this by $C B ∣ u ∣ v^{T} D v$ for one absolute finite $C$ . Choose $C_{0}$ so that $C_{0} \geq C$ and $1 / C_{0} < b$ , and set $τ = C_{0} B$ . Each bounded summand therefore has the asserted derivative bound on $τ ∣ z ∣ < 1$ , using its own covariance.

3.2step 2.2F3F4F5F6algebra

Substitute $u = \sqrt{s} t$ in each requested tail integral, using the constant Jacobian $s^{- d / 2}$ . For $∣ u ∣ \geq a / κ$ , $e^{- γ ∣ u ∣^{2} / 2} \leq e^{- γ a^{2} / (4 κ^{2})} e^{- γ ∣ u ∣^{2} / 4}$ . For every fixed $N$ , the function $z \mapsto z^{N} e^{- γ a^{2} z^{2} / 4}$ is bounded on $z \geq 1$ by differentiation, so the extracted exponential is at most $C_{a, N, γ} κ^{N}$ . The integral of $e^{- γ ∣ u ∣^{2} / 4}$ is finite by the normal density normalization in [F4]; its product with $∣ u ∣$ is integrable as well, since $∣ u ∣ e^{- γ ∣ u ∣^{2} / 8}$ is bounded and the remaining Gaussian is integrable. Using $∣ u \cdot v ∣ \leq ∣ u ∣ ∣ v ∣$ gives the two tail bounds, with an additional $s^{- 1 / 2} ∣ v ∣$ in the weighted bound. Taking the maximum of these constants over $d = 1, 2, 3, 4$ makes them uniform.

4.1step 3.1step 1.2F1algebra

By independence [F1], the moment generating function of $S$ is the product of the factors in steps 1.1 and 1.2. On $τ ∣ z ∣ < 1$ , its logarithm is the sum of the analytic logarithms just constructed, with value zero at zero. Since the covariances add and $\sum_{j} cov (X_{j}) \leq s I_{d}$ , summing step 3.1 gives $∣ K_{u v v} (z) ∣ \leq τ ∣ u ∣ \sum_{j} v^{T} cov (X_{j}) v \leq τ s ∣ u ∣ ∣ v ∣^{2}$ . This proves the analytic assertion, including the empty bounded sum.

5.1step 4.1step 2.2step 3.2F4F5algebra∎

If $A A^{T} = I_{k}$ , the operator norm of $A$ is one: $A^{T}$ is an isometry and $∣ A x ∣ = \sup_{∣ v ∣ = 1} ∣ v \cdot A x ∣ \leq ∣ x ∣$ by [F5]. Thus $A X_{j}$ remains bounded by $B$ and centered, its sum has covariance $s A A^{T} = s I_{k}$ , and $A Z$ is Gaussian with covariance $A G A^{T} \geq γ s I_{k}$ by [F4]. Independence is preserved by applying measurable maps separately. All earlier steps therefore apply to $A S$ with the same $C_{0}$ . The map $(x, y) \mapsto ((x + y) / \sqrt{2}, (x - y) / \sqrt{2})$ is orthogonal because it preserves $∣ x ∣^{2} + ∣ y ∣^{2}$ by expansion; consequently its coordinate prefixes have the required row isometry property. This proves all assertions.

Depends on

Used by

Dependency tree · two levels

76 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

A. Yu. Zaitsev, Estimates of quantiles of smooth conditional distributions and the multidimensional invariance principle, Siberian Mathematical Journal 37 (1996), §§1–2; Gaussian convolution specialization proved here (standard reference, not scraped)