Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Chernoff bound for independent bernoulli trials

Statement

Let X1,…,XN be mutually independent Bernoulli(pi) variables on a finite probability space. Set S=∑iXi and μ=∑ipi. For δ≥0, P(S≥(1+δ)μ)≤exp⁡{−μ((1+δ)log⁡(1+δ)−δ)}. For 0≤δ<1, P(S≤(1−δ)μ)≤exp⁡{−μ(δ+(1−δ)log⁡(1−δ))}. For 0≤δ≤1 the upper and lower tails are respectively at most exp⁡(−μδ2/3) and exp⁡(−μδ2/2), and P(∣S−μ∣≥δμ)≤2exp⁡(−μδ2/3). At δ=1 the lower optimized bound is exp⁡(−μ), proved directly rather than by taking log⁡0. Empty sums and μ=0 are included. Also, for N>0 and t≥0, P(∣S−μ∣≥t)≤2exp⁡(−2t2/N).

Facts & Assumptions

Given: The finite mutually independent family above. No AC is assumed.

[F1]

Bernoulli probabilities are pi and 1−pi at 1 and 0 (Bernoulli random variables and binomial random variables as sums of independent Bernoulli trials).

[F2]

Expectation factors for a finite product of mutually independent variables (Expectation factors over a finite product of mutually independent random variables).

[F3]

Finite-space Markov bounds a nonnegative variable at a positive threshold (Markov's inequality on a finite probability space).

Proof

1.1F4F5F6

The function h(u)=exp⁡(u)−1−u is zero at zero and has derivative exp⁡(u)−1, nonnegative for u≥0 and nonpositive for u≤0. On each compact interval between zero and u it is smooth, so F6 proves h(u)≥0 for either sign of u. Thus 1+u≤exp⁡(u) for every real u.

2.1step 1.1F1F2F4

Functions of distinct independent variables remain mutually independent here: for each prescribed transformed value, sum the original joint probabilities over its finite preimage; the product factorization distributes over these finite sums. Consequently F2 and exponential addition give, for every real λ, EeλS=∏i(1+pi(eλ−1))≤∏iepi(eλ−1)=eμ(eλ−1). Every factor before the inequality is positive, even when pi=0 or 1, so multiplying the inequalities from step 1.1 preserves order.

3.1step 2.1F3F4

For μ>0,δ>0, Markov with λ=log⁡(1+δ)>0 bounds the upper-tail probability by exp⁡(μ(eλ−1)−λ(1+δ)μ), which is exactly the upper displayed expression. For 0<δ<1, take λ=log⁡(1−δ)<0; then S≤(1−δ)μ implies eλS≥eλ(1−δ)μ. Markov with this positive threshold gives the lower displayed expression. At δ=0 both rate expressions are zero and the assertion is just a probability at most one; no positive exponential parameter is needed.

4.1step 3.1F4F5F6

On [0,1] set a(u)=log⁡(1+u)−2u/(2+u). Its derivative is u2/((1+u)(2+u)2)≥0 and a(0)=0, hence log⁡(1+u)≥2u/(2+u)≥2u/3. Therefore the derivative of (1+u)log⁡(1+u)−u−u2/3 is nonnegative and its value at zero is zero. For 0≤u<1, the derivative of −log⁡(1−u)−u is u/(1−u)≥0 and its value at zero is zero. It follows that the derivative of u+(1−u)log⁡(1−u)−u2/2 is nonnegative, with zero initial value. All denominators and logarithm arguments are positive on the compact intervals used. F6 proves the rate bounds u2/3 and u2/2. Substitution in step 3.1 gives the simplified tails away from the lower endpoint u=1.

5.1step 1.1step 4.1F1F2F4

At δ=1, independence gives P(S=0)=∏i(1−pi)≤e−μ by step 1.1, including a zero factor when some pi=1. This also implies the weaker lower bound e−μ/2. If μ=0, every pi=0, so each event Xi=1 has mass zero; summing the finitely many masses shows S=0 almost surely. Both weak multiplicative thresholds then have probability one, matching their bounds one. For N=0 this holds identically by the empty-sum convention. Finally 1A∪B≤1A+1B and finite summation give the union bound. Applying it to upper and lower deviations and using e−μδ2/2≤e−μδ2/3 gives the stated two-sided bound, also at δ=0.

6.1step 5.1F1F4F5F6

For a single Bernoulli(p), put A(λ)=1−p+peλ>0 and g(λ)=log⁡A(λ)−pλ. Direct differentiation gives g(0)=g′(0)=0, g′=q−p and g′′=q(1−q), where q=peλ/A(λ)∈[0,1]. Thus g′′≤1/4, since q(1−q)=1/4−(q−1/2)2. The smooth function v(λ)=g(λ)−λ2/8 has v′′≤0 and v(0)=v′(0)=0. Apply F6 first to v' and then to v on either side of zero: v' is nonincreasing, so v is nondecreasing up to zero and nonincreasing after zero. Hence g(λ)≤λ2/8 for all real λ, including both deterministic p endpoints. Exponentiating yields Eeλ(X−p)≤eλ2/8.

7.1step 2.1step 5.1step 6.1F2F3F4∎

Factor the centered exponential expectation using the independence justification of step 2.1 to obtain Eeλ(S−μ)≤eNλ2/8. For t>0, Markov with λ=4t/N bounds P(S−μ≥t) by e−2t2/N. Apply the same estimate with λ=−4t/N to S−μ≤−t. The union bound from step 5.1 gives the additive assertion. At t=0 its right side is two and is trivially an upper bound. Division by N is licensed by the additive assertion's hypothesis N>0; nothing is asserted from that formula at N=0.

Depends on

Used by

Dependency tree · two levels

54 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