Hoeffding's Theorem 3

Part of MiscMath.Probability.PoissonTrialsFixedMean, whose module docstring states the result, its source and its scope, and where the reader should start. This file proves it: the binomial maximises E[g S] at a fixed mean, for g convex on the integer grid.

Theorem 3: the binomial maximises E[g S] at a fixed mean

For g convex on the integer grid, E[g S] is maximised, among all p with a given mean, by the constant vector — that is, by the binomial.

The proof is Hoeffding's two-coordinate exchange, in a form that terminates. bernExp_pair_le is one exchange: the master identity with a sign supplied, needing only weak grid convexity, with the range hypotheses imposed off the moved pair only (the identity's factor never reads the moved coordinates). exists_move is the move, and it is not the pairwise average, which never terminates for #s ≥ 3; it sends one coordinate exactly to μ and gives its partner the slack, so one more coordinate is pinned at μ at every step and the induction closes in at most #s steps. No compactness, no extreme-value theorem and no limit of iterated averages appears anywhere.

Both halves of p i ∈ [0,1] are load-bearing for the inequality itself, not merely for its interpretation: hoeffding_thm3_needs_le_one and hoeffding_thm3_needs_nonneg are witnesses in which the model's weights are still perfectly well defined and still sum to 1 (sum_bernWt has no hypothesis), yet the inequality reverses.

theorem MiscMath.Probability.bernWt_nonneg {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s A : Finset ι} {p : ι → 𝕜} (hA : A ⊆ s) (h0 : ∀ i ∈ s, 0 ≤ p i) (h1 : ∀ i ∈ s, p i ≤ 1) : 0 ≤ bernWt s p A

theorem MiscMath.Probability.sum_bernWt_secondDiff_nonneg {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {R : Finset ι} {p : ι → 𝕜} (h0 : ∀ i ∈ R, 0 ≤ p i) (h1 : ∀ i ∈ R, p i ≤ 1) {g : ℕ → 𝕜} (hg : ∀ k ≤ R.card, 0 ≤ secondDiff g k) : 0 ≤ ∑ B ∈ R.powerset, bernWt R p B * secondDiff g B.card

The convex factor of the master identity is ≥ 0. The grid range consumed is exactly the posed one: #B + 2 ≤ #R + 2 = #s.

theorem MiscMath.Probability.sum_bernWt_secondDiff_pos {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {R : Finset ι} {p : ι → 𝕜} (h0 : ∀ i ∈ R, 0 ≤ p i) (h1 : ∀ i ∈ R, p i ≤ 1) {g : ℕ → 𝕜} (hg : ∀ k ≤ R.card, 0 < secondDiff g k) : 0 < ∑ B ∈ R.powerset, bernWt R p B * secondDiff g B.card

The strict version: with p in range some weight is positive, because the weights sum to 1, so a strictly convex g makes the factor strictly positive.

theorem MiscMath.Probability.bernExp_pair_le {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) {p q : ι → 𝕜} {g : ℕ → 𝕜} (hout : ∀ k ∈ s, k ≠ i → k ≠ j → q k = p k) (hsum : q i + q j = p i + p j) (hprod : p i * p j ≤ q i * q j) (h0 : ∀ k ∈ s, k ≠ i → k ≠ j → 0 ≤ p k) (h1 : ∀ k ∈ s, k ≠ i → k ≠ j → p k ≤ 1) (hg : ∀ (k : ℕ), k + 2 ≤ s.card → 0 ≤ secondDiff g k) : bernExp s p g ≤ bernExp s q g

The exchange step. A sum-preserving move of two coordinates that does not decrease their product does not decrease bernExp, for g convex on the grid. Only weak convexity is used, and the range hypotheses are imposed off the moved pair only — p i and p j may be anything at all, because the master identity's factor never reads them.

theorem MiscMath.Probability.bernExp_pair_lt {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) {p q : ι → 𝕜} {g : ℕ → 𝕜} (hout : ∀ k ∈ s, k ≠ i → k ≠ j → q k = p k) (hsum : q i + q j = p i + p j) (hprod : p i * p j < q i * q j) (h0 : ∀ k ∈ s, k ≠ i → k ≠ j → 0 ≤ p k) (h1 : ∀ k ∈ s, k ≠ i → k ≠ j → p k ≤ 1) (hg : ∀ (k : ℕ), k + 2 ≤ s.card → 0 < secondDiff g k) : bernExp s p g < bernExp s q g

The strict exchange step: a strictly convex g and a strict increase of the product give a strict increase of bernExp.

theorem MiscMath.Probability.exists_move {ι : Type u_1} {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {p : ι → 𝕜} {μ : 𝕜} (h0 : ∀ k ∈ s, 0 ≤ p k) (h1 : ∀ k ∈ s, p k ≤ 1) (hmean : ∑ k ∈ s, p k = ↑s.card * μ) (hne : ∃ k ∈ s, p k ≠ μ) : ∃ (q : ι → 𝕜) (i : ι) (j : ι), i ∈ s ∧ j ∈ s ∧ i ≠ j ∧ (∀ k ∈ s, 0 ≤ q k) ∧ (∀ k ∈ s, q k ≤ 1) ∧ ∑ k ∈ s, q k = ↑s.card * μ ∧ {k ∈ s | q k ≠ μ}.card < {k ∈ s | p k ≠ μ}.card ∧ (∀ k ∈ s, k ≠ i → k ≠ j → q k = p k) ∧ q i + q j = p i + p j ∧ p i * p j < q i * q j

One step of the induction: from any p not identically μ on s, a sum-preserving pair move that strictly increases the pair product and strictly decreases the number of coordinates away from μ.

This is not the pairwise average: averaging a pair leaves both coordinates off the mean whenever the pair does not straddle it symmetrically, so iterated averaging only converges and never terminates for #s ≥ 3. Instead one coordinate is sent exactly to μ and its partner takes the slack.

theorem MiscMath.Probability.bernExp_le_const {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {p : ι → 𝕜} {g : ℕ → 𝕜} {μ : 𝕜} (h0 : ∀ k ∈ s, 0 ≤ p k) (h1 : ∀ k ∈ s, p k ≤ 1) (hmean : ∑ k ∈ s, p k = ↑s.card * μ) (hg : ∀ (k : ℕ), k + 2 ≤ s.card → 0 ≤ secondDiff g k) : bernExp s p g ≤ bernExp s (fun (x : ι) => μ) g

Theorem 3, the inequality half. For g convex on the integer grid 0, …, #s - 2, the constant vector μ maximises bernExp over all [0,1]-valued p with mean μ. Only weak convexity is assumed.

theorem MiscMath.Probability.bernExp_lt_const {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {p : ι → 𝕜} {g : ℕ → 𝕜} {μ : 𝕜} (h0 : ∀ k ∈ s, 0 ≤ p k) (h1 : ∀ k ∈ s, p k ≤ 1) (hmean : ∑ k ∈ s, p k = ↑s.card * μ) (hg : ∀ (k : ℕ), k + 2 ≤ s.card → 0 < secondDiff g k) (hne : ∃ k ∈ s, p k ≠ μ) : bernExp s p g < bernExp s (fun (x : ι) => μ) g

The strict form. Under strict grid convexity a single coordinate away from μ already forces strict inequality.

theorem MiscMath.Probability.bernExp_eq_const_iff {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {p : ι → 𝕜} {g : ℕ → 𝕜} {μ : 𝕜} (h0 : ∀ k ∈ s, 0 ≤ p k) (h1 : ∀ k ∈ s, p k ≤ 1) (hmean : ∑ k ∈ s, p k = ↑s.card * μ) (hg : ∀ (k : ℕ), k + 2 ≤ s.card → 0 < secondDiff g k) : bernExp s p g = bernExp s (fun (x : ι) => μ) g ↔ ∀ k ∈ s, p k = μ

The equality clause, both directions.

theorem MiscMath.Probability.bernExp_ge_const_concave {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {p : ι → 𝕜} {g : ℕ → 𝕜} {μ : 𝕜} (h0 : ∀ k ∈ s, 0 ≤ p k) (h1 : ∀ k ∈ s, p k ≤ 1) (hmean : ∑ k ∈ s, p k = ↑s.card * μ) (hg : ∀ (k : ℕ), k + 2 ≤ s.card → secondDiff g k ≤ 0) : bernExp s (fun (x : ι) => μ) g ≤ bernExp s p g

The concave companion, free from g ↦ -g: for g concave on the grid the constant vector minimises.

theorem MiscMath.Probability.hoeffding_thm3 {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} (p : ι → 𝕜) (g : ℕ → 𝕜) (h0 : ∀ i ∈ s, 0 ≤ p i) (h1 : ∀ i ∈ s, p i ≤ 1) (hg : ∀ (k : ℕ), k + 2 ≤ s.card → 0 ≤ g (k + 2) - 2 * g (k + 1) + g k) : bernExp s p g ≤ ∑ k ∈ Finset.range (s.card + 1), g k * ↑(s.card.choose k) * ((∑ i ∈ s, p i) / ↑s.card) ^ k * (1 - (∑ i ∈ s, p i) / ↑s.card) ^ (s.card - k)

Hoeffding (1956), Theorem 3. S is the number of successes in the independent trials indexed by s, with success probabilities p, and p̄ is their average. For g convex on the integer grid 0, …, #s - 2,

E[g S] ≤ ∑_{k ≤ #s} g k · C(#s,k) · p̄^k (1 - p̄)^{#s-k}.

The hypothesis is weak grid convexity; the paper asks for strict convexity, which is needed only for the equality clause hoeffding_thm3_eq_iff.

theorem MiscMath.Probability.hoeffding_thm3_eq_iff {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} (p : ι → 𝕜) (g : ℕ → 𝕜) (h0 : ∀ i ∈ s, 0 ≤ p i) (h1 : ∀ i ∈ s, p i ≤ 1) (hg : ∀ (k : ℕ), k + 2 ≤ s.card → 0 < g (k + 2) - 2 * g (k + 1) + g k) : bernExp s p g = ∑ k ∈ Finset.range (s.card + 1), g k * ↑(s.card.choose k) * ((∑ i ∈ s, p i) / ↑s.card) ^ k * (1 - (∑ i ∈ s, p i) / ↑s.card) ^ (s.card - k) ↔ ∀ i ∈ s, p i = (∑ j ∈ s, p j) / ↑s.card

The equality clause: under strict grid convexity, equality holds exactly when every p i equals the average.

Necessity witnesses for Theorem 3

Each hypothesis of Theorem 3 is load-bearing, and each of the three witnesses below is a machine-checked instance rather than an assertion. The two range witnesses are worth reading carefully: the model's weights are perfectly well defined outside [0,1] and still sum to 1 (sum_bernWt has no hypothesis at all), so what fails is bernWt ≥ 0 — and then the inequality reverses.

theorem MiscMath.Probability.hoeffding_thm3_eq_needs_strict : (∀ (k : ℕ), k + 2 ≤ (Finset.range 2).card → 0 ≤ secondDiff (fun (m : ℕ) => ↑m) k) ∧ (∑ j ∈ Finset.range 2, if j = 0 then 0 else 1) = ↑(Finset.range 2).card * (1 / 2) ∧ ((bernExp (Finset.range 2) (fun (j : ℕ) => if j = 0 then 0 else 1) fun (m : ℕ) => ↑m) = bernExp (Finset.range 2) (fun (x : ℕ) => 1 / 2) fun (m : ℕ) => ↑m) ∧ ¬∀ j ∈ Finset.range 2, (if j = 0 then 0 else 1) = 1 / 2

The strictness in the convexity hypothesis is load-bearing exactly where the equality clause needs it, and nowhere else. At #s = 2 with g = id — convex on the grid (secondDiff g ≡ 0) but not strictly — p = (0,1) has mean 1/2, both sides are equal, and p is not constant. So bernExp_eq_const_iff genuinely needs 0 < secondDiff g k, while bernExp_le_const is unaffected.

theorem MiscMath.Probability.hoeffding_thm3_needs_le_one : (∀ j ∈ Finset.range 3, 0 ≤ if j = 2 then 0 else 3 / 2) ∧ (¬∀ j ∈ Finset.range 3, (if j = 2 then 0 else 3 / 2) ≤ 1) ∧ (∀ (k : ℕ), k + 2 ≤ (Finset.range 3).card → 0 < secondDiff (fun (m : ℕ) => if m = 2 then 5 else if m = 3 then 11 else 0) k) ∧ (∑ j ∈ Finset.range 3, if j = 2 then 0 else 3 / 2) = ↑(Finset.range 3).card * 1 ∧ (bernExp (Finset.range 3) (fun (x : ℕ) => 1) fun (m : ℕ) => if m = 2 then 5 else if m = 3 then 11 else 0) < bernExp (Finset.range 3) (fun (j : ℕ) => if j = 2 then 0 else 3 / 2) fun (m : ℕ) => if m = 2 then 5 else if m = 3 then 11 else 0

The bound p i ≤ 1 cannot be dropped, and not merely for interpretation: the inequality reverses. Witness at #s = 3: p = (3/2, 3/2, 0), which keeps 0 ≤ p i and has mean 1, against g = (0,0,5,11), strictly convex on the grid (secondDiff g = (5,1)). The left-hand side is 45/4, the comparator is 11.

This is not a counterexample to Theorem 3: p is not a probability vector, so the witness lies outside the theorem's setting. It records that the setting is load-bearing for the mathematics, not only for the reading.

theorem MiscMath.Probability.hoeffding_thm3_needs_nonneg : (∀ j ∈ Finset.range 3, (if j = 2 then 1 else -1) ≤ 1) ∧ (¬∀ j ∈ Finset.range 3, 0 ≤ if j = 2 then 1 else -1) ∧ (∀ (k : ℕ), k + 2 ≤ (Finset.range 3).card → 0 < secondDiff (fun (m : ℕ) => if m = 2 then 1 else if m = 3 then 7 else 0) k) ∧ (∑ j ∈ Finset.range 3, if j = 2 then 1 else -1) = ↑(Finset.range 3).card * (-1 / 3) ∧ (bernExp (Finset.range 3) (fun (x : ℕ) => -1 / 3) fun (m : ℕ) => if m = 2 then 1 else if m = 3 then 7 else 0) < bernExp (Finset.range 3) (fun (j : ℕ) => if j = 2 then 1 else -1) fun (m : ℕ) => if m = 2 then 1 else if m = 3 then 7 else 0

The other bound 0 ≤ p i cannot be dropped either, so neither half of p i ∈ [0,1] is redundant. Witness at #s = 3: p = (-1,-1,1), which keeps p i ≤ 1 and has mean -1/3, against g = (0,0,1,7), strictly convex on the grid (secondDiff g = (1,5)). The left-hand side is 3, the comparator is 5/27.