LemmaStatement: Literature-sourcedProof: 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.

The Hoeffding MGF bound for a variable in a unit interval

Statement

Let $Y$ be a measurable real random variable on a probability space with $0 \leq Y \leq 1$ almost surely. Then, for every $λ \in R$ ,

$E \exp {λ (Y - E Y)} \leq \exp (λ^{2} / 8) .$

This proof uses only finite product and scalar integral arguments; it does not assume the Axiom of Choice.

Facts & Assumptions

Given: A probability space, a measurable $Y$ with $0 \leq Y \leq 1$ almost surely, and $λ \in R$ .

[F1]

If $X \leq W$ almost surely for integrable real variables, then $E X \leq E W$ (Linearity, monotonicity, and the modulus bound for expectation).

[F2]

For $0 \leq t \leq 1$ and real $x, y$ , $\exp ((1 - t) x + t y) \leq (1 - t) \exp (x) + t \exp (y)$ (The two-point convexity inequality for the exponential function).

[F3]

For $u > 0$ , $\log$ is differentiable and $\log^{'} (u) = 1 / u$ ; $\exp^{'} = \exp$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, The exponential function is smooth and $(\exp)^{'} = \exp$ ).

[F4]

Sums, scalar multiples, products, quotients with nonzero denominator, and compositions obey the usual derivative and continuity rules (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).

[F5]

If a differentiable function has continuous integrable derivative on a compact interval, the second fundamental theorem evaluates the integral of that derivative by endpoint differences (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[F6]

The exponential is positive, $\exp (0) = 1$ , and $\log (1) = 0$ (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F7]

A real-valued function is measurable when all strict upper or all strict lower threshold sets are measurable; the exponential is strictly increasing, positive, and inverse to the natural logarithm on positive inputs (Threshold characterisations of real-valued and extended-real-valued measurability, The exponential function is strictly increasing, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The natural logarithm as the inverse of the exponential function).

[F8]

The exponential addition formula is $\exp (x + y) = \exp (x) \exp (y)$ (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ ).

[F9]

Absolute values of measurable real functions are measurable. A statement holding almost surely has a measurable null exceptional set. The probability measure satisfies $P (Ω) = 1$ . For nonnegative measurable $g$ , the set function $B \mapsto \int_{B} g d P$ is a measure; the nonnegative integral is monotone under pointwise order, indicators integrate to their measures, and integrals over null sets vanish. A real measurable function is integrable exactly when its absolute-value integral is finite (Arithmetic and lattice operations preserve measurability whenever they are defined, Measure-null sets and almost-everywhere statements relative to a measure, Probability measures and probability spaces, The indefinite integral of a nonnegative measurable function is a measure, Integral over a measurable subset, Monotonicity and nonnegative homogeneity of the nonnegative integral, The integral of a nonnegative simple function, A nonnegative integral over a null set vanishes, Integrable real and complex functions, and their integrals).

Proof

Given: A probability space, a measurable $Y$ with $0 \leq Y \leq 1$ almost surely, and $λ \in R$ .

1.1F6F7givenalgebra

Let $X$ be any measurable real random variable. For $a < 0$ , ${e^{λ X} > a}$ is the whole probability space by [F6]. For $a \geq 0$ and $λ = 0$ , this set is the whole space if $a < 1$ and empty if $a \geq 1$ . For $a \geq 0$ and $λ \neq 0$ , it is the whole space when $a = 0$ ; when $a > 0$ , strict increase of the exponential and the inverse relation with $\log$ give ${e^{λ X} > a} = {\begin{cases} {X > (\log a) / λ}, & λ > 0, \\ {X < (\log a) / λ}, & λ < 0. \end{cases}$ Every set on the right is measurable by [F7]. Thus $e^{λ X}$ is measurable by the threshold characterization, with no appeal to a continuous-map Borel measurability result qualified by Countable Choice.

2.1F1F2F9step 1.1given

Let $A : = {∣ Y ∣ \leq 1}$ , measurable by [F9], so $P (A) = 1$ . Define $ν (B) : = \int_{B} ∣ Y ∣ d P$ ; by [F9] this is a measure. Since $∣ Y ∣ 1_{A} \leq 1_{A}$ , [F9] gives $ν (A) \leq P (A) = 1$ , while $P (A^{c}) = 0$ gives $ν (A^{c}) = 0$ . Therefore $E ∣ Y ∣ = ν (Ω) = ν (A) + ν (A^{c}) \leq 1$ , so $Y$ is integrable by [F9]. Put $p : = E Y$ ; then [F1] gives $p \in [0, 1]$ . The shifted variable $Y - p$ is measurable because ${Y - p > a} = {Y > a + p}$ for every real $a$ . Applying step 1.1 to $X = Y$ and $X = Y - p$ establishes measurability of both exponentials. Applying [F2] with endpoints $0, λ$ gives $e^{λ y} \leq 1 - y + y e^{λ}$ for every $y \in [0, 1]$ ; taking expectations yields $E e^{λ Y} \leq 1 - p + p e^{λ}$ .

3.1givenF3F4F6step 2.1algebra

Define $g (λ) : = 1 - p + p e^{λ} > 0$ and $ψ (λ) : = \log g (λ) - p λ$ . Positivity follows from [F6] and $p \in [0, 1]$ . With $q (λ) : = p e^{λ} / g (λ) \in [0, 1]$ , [F3]–[F4] give $ψ (0) = ψ^{'} (0) = 0$ and $ψ^{''} (λ) = q (λ) (1 - q (λ)) \in [0, 1 / 4]$ . The formula also covers $p = 0$ or $p = 1$ , since then $g$ remains positive.

4.1F5step 3.1algebra

The function $ψ^{''}$ in step 3.1 is continuous. For $λ \geq 0$ , integrating twice by [F5] gives $ψ (λ) = \int_{0}^{λ} (λ - s) ψ^{''} (s) d s \leq λ^{2} / 8$ . For $λ < 0$ , the same endpoint formula written from $λ$ to $0$ gives $ψ (λ) = \int_{λ}^{0} (s - λ) ψ^{''} (s) d s \leq λ^{2} / 8$ .

5.1F8step 2.1step 4.1algebra∎

By step 2.1 and the exponential addition formula [F8], $E e^{λ (Y - p)} = e^{- λ p} E e^{λ Y} \leq e^{- λ p} g (λ) = e^{ψ (λ)}$ ; step 4.1 bounds this by $e^{λ^{2} / 8}$ . This proves the claim for every real $λ$ , including $λ = 0$ .

Depends on

Used by

Dependency tree · two levels

97 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, Lemma 1.8 (standard reference, not scraped)
John Duchi, Lecture Notes on Statistics and Information Theory, Chapter 4, Hoeffding's Lemma (standard reference, not scraped)