Hoeffding's Theorem 4, in its two extreme regimes #
Part of MiscMath.Probability.PoissonTrialsFixedMean, whose module docstring states the
result, its source and — importantly here — the scope of what is and is not claimed, and
where the reader should start. This file proves the two extreme regimes of Theorem 4, the
trivial bounds and the complement duality that accompany them, the attainment of all four
bounds, and the size of the regime that is left out.
Theorem 4: the tail against the binomial, away from the mean #
If the mean number of successes is lam, then k ≥ lam ⟹ P[S ≤ k] ≥ B(k; n, lam/n) and
k ≤ lam - 1 ⟹ P[S ≤ k] ≤ B(k; n, lam/n), with n the number of trials. So among all trial
vectors with the given mean, the homogeneous one has the lightest lower tail at thresholds
k ≥ lam and the heaviest at thresholds k ≤ lam - 1. The second regime is k ≤ lam - 1
and not k < lam; thm4_lower_needs_le_sub_one shows the difference is real.
The idea in one line. Corollary 2.1 reduces the theorem to the extremal shapes — a
coordinates at 1, b at 0, r at a common x — and there both halves are the same
statement about one potential. With m + 1 trials, threshold k and mean lam,
Φ(t) = B(k; m+1, t) + (m+1)·(t - lam/(m+1))·C(m,k)·t^k·(1-t)^(m-k),
so that Φ(lam/(m+1)) is the binomial itself, Φ(lam/m) is the drop-a-zero comparator and
Φ((lam-1)/m) is the drop-a-one comparator: three points of one curve. And
Φ'(t) = (m+1)·C(m,k)·(t - lam/(m+1))·h'(t), h(t) = t^k (1-t)^(m-k),
because C(m,k)·h is exactly minus the derivative of the binomial tail
(hasDerivAt_binTail), so the two unbracketed terms cancel. The whole of Theorem 4 is
therefore the sign of h', which changes once, at m·t = k; every hypothesis of the four
families below is exactly what puts the relevant interval on one side of that.
The four families are stated at m + 1 trials and, where a threshold drops, at k + 1,
so that no ℕ-subtraction appears in them. That is not cosmetic: written with k - 1, the
drop-a-one family of the upper half is false at k = 0, where the truncation turns the
empty tail into the full one, and it then needs a 1 ≤ k guard. Stated at k + 1 the
offending cell cannot be expressed, so no guard is needed.
The potential. lam is the mean, m + 1 the number of trials, k the
threshold. The added term vanishes at t = lam/(m+1) and is engineered so that
the derivative of the tail cancels against it.
Equations
- MiscMath.Probability.binPot m k lam t = MiscMath.Probability.binTail (m + 1) t k + (↑m + 1) * (t - lam / (↑m + 1)) * (↑(m.choose k) * MiscMath.Probability.binShape k m t)
Instances For
The sign of h', on the OPEN interval #
The closed-interval form of binShapeD_nonpos would be false: at t = 1, k = m the
hypothesis k ≤ m·t holds while C(m,m)·h'(1) = m > 0. Both endpoints are excluded here,
and monotoneOn_of_deriv_nonneg asks for the sign on interior only, so nothing is lost.
The four one-parameter families #
Each is a comparison of two binomial tails at matched means, one with a coordinate
dropped: lam/(m+1) against lam/m (a coordinate pinned at 0) or against (lam-1)/m (a
coordinate pinned at 1).
Drop a zero, below the mean — the mirror of
binTail_succ_le_binTail_dropZero. The hypothesis 0 ≤ lam of the mirror is
not needed here: (k : ℝ) ≤ lam - 1 with k : ℕ already forces lam ≥ 1.
Drop a one, below the mean — the mirror of
binTail_succ_le_binTail_dropOne. Stated at threshold k + 1, which is where
the 1 ≤ k guard of the k - 1 phrasing went.
The pure-binomial residue #
With Corollary 2.1 discharging the extremal structure, what is left of Theorem 4 is a
statement about binTail alone: a coordinates at 1, r at x, the remaining
n - a - r at 0, so the mean is lam = a + r·x. It follows from the four families by
induction on n, dropping one coordinate at a time.
The residue, below the mean. The extra hypothesis a ≤ k is real: below
the mean it does not follow from k ≤ lam - 1, and where it fails the model
tail is identically zero — see tailLe_eq_zero_of_lt, which is how
tailLe_le_binTail covers that branch.
Theorem 4, above the mean. For independent trials indexed by an
arbitrary s, with success probabilities p and mean lam = ∑ p, and any k ≥ lam,
B(k; #s, lam/#s) ≤ P[S ≤ k].
No hypothesis beyond 0 ≤ p i ≤ 1 on s.
Theorem 4, below the mean. For k ≤ lam - 1, P[S ≤ k] ≤ B(k; #s, lam/#s).
The trivial bounds, and the complement duality #
Hoeffding's (24) and (26) each pair a substantial bound with a trivial one — 0 ≤ P[S ≤ c]
and P[S ≤ c] ≤ 1 — and the paper's proof gets each lower bound from an upper bound through
the identity P(S ≤ c | p) = 1 - P(S ≤ n-c-1 | 1-p). Both are recorded here: the trivial
bounds because they are part of the displayed statement, and the duality because it is the
symmetry of the whole section, and is stated without ℕ-subtraction.
P[S ≤ k] is nonnegative.
P[S ≤ k] is at most 1.
Complementation A ↦ s \ A is an involution of s.powerset, so it leaves any sum over
the powerset unchanged.
Complementing the trials complements the success sets. Replacing every p i by
1 - p i and every success set A by s \ A leaves the weight unchanged.
The complement duality, in the form Hoeffding uses (p. 720): with n = #s trials,
P[S ≤ k | p] = 1 - P[S ≤ n - k - 1 | 1 - p]. Stated as k + j + 1 = n so that no
ℕ-subtraction appears.
Theorem 4, packaged, and the sharpness of its bounds #
hoeffding_thm4 puts the two regimes together in the shape of the paper's (24) and (26),
trivial bounds included. The three exists_inBox_* theorems then discharge the paper's
assertion that all four of those bounds are attained: each is realised by an explicit
point of the fixed-mean box, so none of them can be improved. (The uniqueness half of the
paper's attainment statement — that some of them are attained only at the constant vector —
is not formalised; see the caveat in the module docstring.)
Hoeffding (1956), Theorem 4 — the two extreme regimes, with no hypothesis beyond the box, on an arbitrary ground set.
tailLe s p k is P[S ≤ k] for independent trials with success probabilities p, and
binTail #s (lam/#s) k is the same for #s identical trials at the common mean. The
comparison holds in one direction at thresholds k ≥ lam and the other at k ≤ lam - 1,
and the trivial bound of the paper's display accompanies each.
Not claimed: the middle regime lam - 1 < k < lam of the paper's (25), and the equality
clause of the paper's attainment statement. The middle regime is empty or a single
threshold: see thm4_gap_subsingleton.
Theorem 4 on range n, the form in which it is usually quoted.
The binomial bound of Theorem 4 is attained, in either regime: the constant vector
p ≡ lam/#s lies in the fixed-mean box and its tail is the binomial tail. So neither
inequality of hoeffding_thm4 can be strengthened.
The upper bound 1 of the paper's (26) is attained. Above the mean there is a point
of the fixed-mean box at which P[S ≤ k] = 1: pin ⌊lam⌋ trials at success, give the
fractional remainder to one further trial, and leave the rest at 0.
The lower bound 0 of the paper's (24) is attained. Below the mean there is a point
of the fixed-mean box at which P[S ≤ k] = 0: pin k + 1 trials at success — which the
regime k ≤ lam - 1 leaves room for — and spread the remaining mean evenly over the rest.
What the two regimes leave out #
The paper's Theorem 4 has a third regime, lam - 1 < c < lam, whose bound is the auxiliary
Q(c,p) of its (27); that regime is not formalised here. What is formalised is its size.
Since the threshold is an integer and the regime is an open interval of length 1, it
contains at most one integer, namely ⌊lam⌋, and none at all when the mean is a whole
number. So the two bounds above cover every threshold but one, and cover all of them
whenever lam ∈ ℕ.
When the mean is a whole number the uncovered regime is empty, so the two bounds of
hoeffding_thm4 between them settle every threshold.
The lower regime cannot be widened to "below the mean". Its hypothesis is
k ≤ lam - 1, and the difference from k < lam is not slack. At p = (1, 1/2) on two
trials the mean is 3/2, and the threshold k = 1 lies below it but outside the regime:
there P[S ≤ 1] = 1/2 while B(1; 2, 3/4) = 7/16, so the binomial tail is the lighter
one and the inequality of tailLe_le_binTail runs the other way.
So the gap lam - 1 < k < lam is not merely a regime nobody attempted. It is where the
looser reading is false, which is why hoeffding_thm4 carries the hypothesis it does.