TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Sub-exponential concentration for independent sums

Statement

Let $X_{1}, \dots, X_{n}$ be independent centered real random variables, with $X_{i}$ sub-exponential with parameters $(ν_{i}^{2}, b_{i})$ as defined in Sub-Gaussian variables and vectors, and sub-exponential variables, where $n \geq 1$ and $b_{i} > 0$ . Put $v = \sum_{i = 1}^{n} ν_{i}^{2}$ , $b = \max_{1 \leq i \leq n} b_{i}$ , and $S = \sum_{i = 1}^{n} X_{i}$ . For $t > 0$ , if $v > 0$ then $P (∣ S ∣ \geq t) \leq 2 \exp ⁣ (- \frac{1}{2} \min ⁣ {\frac{t^{2}}{v}, \frac{t}{b}}),$ and if $v = 0$ then $P (∣ S ∣ \geq t) = 0$ .

Facts & Assumptions

Given: Independent centered real random variables $X_{i}$ with sub-exponential parameters $(ν_{i}^{2}, b_{i})$ , where $ν_{i}^{2} \geq 0$ and $b_{i} > 0$ .

[F1]

Sub-exponentiality means $E e^{λ X_{i}} \leq e^{λ^{2} ν_{i}^{2} / 2}$ whenever $∣ λ ∣ \leq 1 / b_{i}$ (Sub-Gaussian variables and vectors, and sub-exponential variables).

[F2]

Independence means independence of the sigma-algebras generated by the variables (Independent random elements).

[F3]

For independent real variables and nonnegative Borel functions, the expectation of the product factors (Expectations factor over finite products of independent random variables).

[F4]

Markov's inequality gives $P (Y \geq r) \leq E [Y] / r$ for $Y \geq 0$ and $r > 0$ (Markov's inequality for random variables).

[F5]

The exponential is continuous and strictly increasing, positive, satisfies $e^{- x} = 1 / e^{x}$ and $e^{x + y} = e^{x} e^{y}$ , and has $e^{0} = 1$ ; these imply $e^{x} + e^{- x} - 2 = e^{- x} (e^{x} - 1)^{2} \geq 0$ , with equality only at $x = 0$ (The real exponential function and the number $e$ by a power series, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The exponential function is strictly increasing).

[F6]

A nonnegative integrable function with integral $0$ vanishes almost everywhere (A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere).

[F7]

Probability is subadditive on finite unions (Basic identities for a probability measure).

[F8]

A nonempty finite set of real numbers has a maximum (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[F9]

Expectation is linear on integrable real random variables (Linearity, monotonicity, and the modulus bound for expectation).

[F10]

Finite sums of real-valued measurable functions are measurable (Arithmetic and lattice operations preserve measurability whenever they are defined).

Proof

1.1givenF1F5F6F7F9F10algebra

If $v = 0$ , then every $ν_{i}^{2} = 0$ . Fix $i$ and choose $λ_{i} = 1 / (2 b_{i}) > 0$ . By [F1], both $E e^{λ_{i} X_{i}}$ and $E e^{- λ_{i} X_{i}}$ are at most $1$ . The nonnegative random variable $Q_{i} = e^{λ_{i} X_{i}} + e^{- λ_{i} X_{i}} - 2$ therefore has expectation at most $0$ by [F9]. By [F5], $Q_{i} = 0$ only when $X_{i} = 0$ ; [F6] gives $X_{i} = 0$ almost surely. The finite sum $S$ is consequently $0$ almost surely by [F7].

1.2F1F2F3F5F8givenconstruct

Suppose $v > 0$ . By [F8], $b = \max_{i} b_{i}$ exists and is positive. For each real $θ$ , the map $g_{θ} (x) = e^{θ x}$ is continuous: scalar multiplication is continuous since $∣ θ x - θ y ∣ = ∣ θ ∣ ∣ x - y ∣$ , and the exponential is continuous by [F5]. Its inverse images of open sets are open, so the collection of Borel sets with Borel preimage is a sigma-algebra containing the opens; hence $g_{θ}$ is Borel by The Borel sigma-algebra of a topological space, For each Borel $B$ , ${g_{θ} (X_{i}) \in B} = X_{i}^{- 1} (g_{θ}^{- 1} (B))$ is measurable. For $0 \leq λ \leq 1 / b$ , [F1] applies to every $X_{i}$ . By [F5], $e^{λ S} = \prod_{i} e^{λ X_{i}}$ ; independence [F2] and factorization [F3] give $E e^{λ S} = \prod_{i} E e^{λ X_{i}} \leq e^{λ^{2} v / 2}$ .

2.1F4F5F10step 1.2algebra

For $t > 0$ and $0 < λ \leq 1 / b$ , [F10] makes $S$ a measurable real random variable, and $S \geq t$ implies $e^{λ S} \geq e^{λ t} > 0$ by [F5]. Markov [F4], step 1.2, and the reciprocal and addition formulas in [F5] yield $P (S \geq t) \leq \exp (- λ t + λ^{2} v / 2)$ . Choose $λ = \min {t / v, 1 / b}$ . If $t \leq v / b$ , the exponent is $- t^{2} / (2 v)$ . If $t > v / b$ , it is $- t / b + v / (2 b^{2}) \leq - t / (2 b)$ . Hence $P (S \geq t) \leq \exp [- \frac{1}{2} \min {t^{2} / v, t / b}]$ .

3.1F1F2F3F4F5F7F10step 1.1step 1.2step 2.1algebra∎

For $0 < λ \leq 1 / b$ , [F1] applies at parameter $- λ$ to every original $X_{i}$ . By [F5], $e^{- λ S} = \prod_{i} e^{- λ X_{i}}$ ; the original variables are independent by [F2], the functions $x \mapsto e^{- λ x}$ are nonnegative Borel by step 1.2, and factorization [F3] gives $E e^{- λ S} \leq e^{λ^{2} v / 2}$ . Markov [F4] and the same optimizing choice as in step 2.1 yield the stated lower-tail bound. The finite union bound [F7] combines the tails; step 1.1 handles $v = 0$ . No independence assertion about the transformed variables is needed.

Depends on

Used by

Dependency tree · two levels

78 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

Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Chapter 1, §1.3, Theorem 1.13 (standard reference, not scraped)
John Duchi, Lecture Notes on Statistics and Information Theory, Chapter 4, §4.1.2 (standard reference, not scraped)