Hoeffding's Corollary 2.1

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 extrema of E[g S] over the fixed-mean box are attained where the coordinates take at most one interior value.

Corollary 2.1: the extremal shapes at a fixed mean

Over the fixed-mean box

InBox s lam p  ↔  (∀ i ∈ s, 0 ≤ p i ≤ 1)  ∧  ∑_{i ∈ s} p i = lam,

the extrema of p ↦ bernExp s p g — for an arbitrary g, with no convexity — are attained at points whose coordinates take at most the three values {0, x, 1}: at most one value is interior.

"At most one interior value" is not "at most one interior coordinate". The interior value may be repeated, and the second reading — which says p is a vertex of the box — is false: bernExp is multi-affine, not convex, so its maximum over a polytope need not sit at a vertex. Both a general refutation and a concrete rational one are below (vertex_reduction_fails_of_strictConvex, vertex_reduction_false), and at the refuting witness the correct form does hold (exHalf_atMostOneInteriorValue).

The proof is a terminating spread reduction, not a compactness argument. exists_spread_move: for an interior pair at fixed sum σ, the spread endpoint (0 and σ when σ ≤ 1; 1 and σ - 1 when σ ≥ 1) stays in the box, strictly decreases the pair product, and strictly decreases the number of interior coordinates. exists_spread_reduction: so from any p in the box, at most #s spread moves reach a q with bernExp p ≤ bernExp q at which every interior pair has 0 < pairFactor. eq_of_pairFactor_pos_of_isMaxOn: at a maximiser a pair with 0 < pairFactor must already be equal, since the equalising move raises the pair product by ((p i - p j)/2)². Compactness enters in exactly one place, and only over ℝ: the existence of a maximiser (exists_isMaxOn_bernExp). Everything before that is field-generic and finite.

def MiscMath.Probability.InBox {ι : Type u_1} {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] (s : Finset ι) (lam : 𝕜) (p : ι → 𝕜) : Prop

The fixed-mean box {p | 0 ≤ p ≤ 1 on s, ∑_{s} p = lam}.

Equations

• MiscMath.Probability.InBox s lam p = ((∀ i ∈ s, 0 ≤ p i) ∧ (∀ i ∈ s, p i ≤ 1) ∧ ∑ i ∈ s, p i = lam)

def MiscMath.Probability.interiorCoords {ι : Type u_1} {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] (s : Finset ι) (p : ι → 𝕜) : Finset ι

The coordinates of p strictly inside (0,1). Inside the box this is exactly "not in {0,1}".

Equations

• MiscMath.Probability.interiorCoords s p = {i ∈ s | 0 < p i ∧ p i < 1}

theorem MiscMath.Probability.interiorCoords_subset {ι : Type u_1} {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] {s : Finset ι} {p : ι → 𝕜} {i : ι} (h : i ∈ interiorCoords s p) : i ∈ s

theorem MiscMath.Probability.mem_interiorCoords {ι : Type u_1} {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] {s : Finset ι} {p : ι → 𝕜} {i : ι} : i ∈ interiorCoords s p ↔ i ∈ s ∧ 0 < p i ∧ p i < 1

def MiscMath.Probability.AtMostOneInteriorValue {ι : Type u_1} {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] (s : Finset ι) (p : ι → 𝕜) : Prop

Hoeffding's shape: at most one interior value, so the coordinates take at most the three values {0, x, 1} — the interior value may be repeated.

Equations

• MiscMath.Probability.AtMostOneInteriorValue s p = ∀ i ∈ MiscMath.Probability.interiorCoords s p, ∀ j ∈ MiscMath.Probability.interiorCoords s p, p i = p j

def MiscMath.Probability.AtMostOneInteriorCoord {ι : Type u_1} {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] (s : Finset ι) (p : ι → 𝕜) : Prop

At most one interior coordinate — equivalently, p is a vertex of the box. This is the reading that vertex_reduction_false refutes.

Equations

• MiscMath.Probability.AtMostOneInteriorCoord s p = ((MiscMath.Probability.interiorCoords s p).card ≤ 1)

def MiscMath.Probability.pairFactor {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] (s : Finset ι) (p : ι → 𝕜) (g : ℕ → 𝕜) (i j : ι) : 𝕜

The factor ∑_{B ⊆ s \ {i,j}} bernWt B · Δ²g(#B) of the master identity. It never reads p i or p j.

Equations

• MiscMath.Probability.pairFactor s p g i j = ∑ B ∈ (s \ {i, j}).powerset, MiscMath.Probability.bernWt (s \ {i, j}) p B * MiscMath.Probability.secondDiff g B.card

theorem MiscMath.Probability.bernExp_pair_move {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [CommRing 𝕜] {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) : bernExp s q g - bernExp s p g = (q i * q j - p i * p j) * pairFactor s p g i j

The master identity, on a ground set. Along a sum-preserving move of the pair (i,j), bernExp changes by the change in the pair product times pairFactor. No sign hypothesis and no convexity.

theorem MiscMath.Probability.update_pair_left {ι : Type u_1} [DecidableEq ι] {β : Type u_3} {p : ι → β} {i j : ι} (hij : i ≠ j) (a b : β) : Function.update (Function.update p i a) j b i = a

theorem MiscMath.Probability.update_pair_right {ι : Type u_1} [DecidableEq ι] {β : Type u_3} {p : ι → β} {i j : ι} (a b : β) : Function.update (Function.update p i a) j b j = b

theorem MiscMath.Probability.update_pair_other {ι : Type u_1} [DecidableEq ι] {β : Type u_3} {p : ι → β} {i j : ι} (a b : β) {k : ι} (hki : k ≠ i) (hkj : k ≠ j) : Function.update (Function.update p i a) j b k = p k

theorem MiscMath.Probability.sum_eq_of_pair_move {ι : Type u_1} {𝕜 : Type u_2} [CommRing 𝕜] {s : Finset ι} {i j : ι} (his : i ∈ s) (hjs : j ∈ s) (hij : i ≠ j) {p q : ι → 𝕜} (hout : ∀ k ∈ s, k ≠ i → k ≠ j → q k = p k) (hsum : q i + q j = p i + p j) : ∑ k ∈ s, q k = ∑ k ∈ s, p k

A sum-preserving pair move preserves the total sum over s.

theorem MiscMath.Probability.interiorCoords_card_lt {ι : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] {s : Finset ι} {p q : ι → 𝕜} {i j : ι} (hi : i ∈ interiorCoords s p) (hj : j ∈ interiorCoords s p) (hqi : ¬(0 < q i ∧ q i < 1)) (hout : ∀ k ∈ s, k ≠ i → k ≠ j → q k = p k) : (interiorCoords s q).card < (interiorCoords s p).card

The interior count strictly drops when one member of an interior pair is pushed out of (0,1) and nothing outside the pair moves.

theorem MiscMath.Probability.exists_spread_move {ι : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {lam : 𝕜} {p : ι → 𝕜} (hp : InBox s lam p) {i j : ι} (hi : i ∈ interiorCoords s p) (hj : j ∈ interiorCoords s p) (hij : i ≠ j) : ∃ (q : ι → 𝕜), InBox s lam q ∧ (∀ k ∈ s, k ≠ i → k ≠ j → q k = p k) ∧ q i + q j = p i + p j ∧ q i * q j < p i * p j ∧ (interiorCoords s q).card < (interiorCoords s p).card

The spread move. For an interior pair at fixed sum σ, send one coordinate to 0 (when σ ≤ 1) or to 1 (when σ ≥ 1) and give the partner the slack. The move stays in the box, strictly decreases the pair product, and strictly decreases the number of interior coordinates — so it terminates in at most #s steps.

theorem MiscMath.Probability.exists_spread_reduction {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {lam : 𝕜} {g : ℕ → 𝕜} {p : ι → 𝕜} (hp : InBox s lam p) : ∃ (q : ι → 𝕜), InBox s lam q ∧ bernExp s p g ≤ bernExp s q g ∧ ∀ i ∈ interiorCoords s q, ∀ j ∈ interiorCoords s q, i ≠ j → 0 < pairFactor s q g i j

The spread reduction. From any p in the box, finitely many value-non-decreasing spread moves reach a q in the box on which every interior pair has a strictly positive pairFactor. The induction is on the interior count, so it terminates in at most #s steps: no compactness, no topology.

theorem MiscMath.Probability.eq_of_pairFactor_pos_of_isMaxOn {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {lam : 𝕜} {g : ℕ → 𝕜} {p : ι → 𝕜} (hp : InBox s lam p) (hmax : ∀ (r : ι → 𝕜), InBox s lam r → bernExp s r g ≤ bernExp s p g) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) (hF : 0 < pairFactor s p g i j) : p i = p j

The pair criterion. At a maximiser, a pair with 0 < pairFactor must already be equal: otherwise the equalising move — which raises the pair product by ((p i - p j)/2)² — strictly increases bernExp. Note the hypotheses: i and j need only be distinct members of s; interiority is not used.

theorem MiscMath.Probability.exists_max_atMostOneInteriorValue {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {lam : 𝕜} {g : ℕ → 𝕜} {p : ι → 𝕜} (hp : InBox s lam p) (hmax : ∀ (r : ι → 𝕜), InBox s lam r → bernExp s r g ≤ bernExp s p g) : ∃ (q : ι → 𝕜), InBox s lam q ∧ bernExp s q g = bernExp s p g ∧ AtMostOneInteriorValue s q

Corollary 2.1, in reduction form. Every maximiser of bernExp over the fixed-mean box can be moved — without changing the value, so the image is again a maximiser — to one whose coordinates take at most the three values {0, x, 1}. Compactness enters only through the hypothesis hmax (that a maximiser exists at all); the reduction itself is finite and constructive.

theorem MiscMath.Probability.exists_min_atMostOneInteriorValue {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {lam : 𝕜} {g : ℕ → 𝕜} {p : ι → 𝕜} (hp : InBox s lam p) (hmin : ∀ (r : ι → 𝕜), InBox s lam r → bernExp s p g ≤ bernExp s r g) : ∃ (q : ι → 𝕜), InBox s lam q ∧ bernExp s q g = bernExp s p g ∧ AtMostOneInteriorValue s q

The minimum direction, by negating g, so nothing new is assumed.

theorem MiscMath.Probability.vertex_reduction_fails_of_strictConvex {ι : Type u_1} [DecidableEq ι] {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {g : ℕ → 𝕜} {μ : 𝕜} (hg : ∀ (k : ℕ), k + 2 ≤ s.card → 0 < secondDiff g k) (hμ0 : 0 < μ) (hμ1 : μ < 1) (hs : 2 ≤ s.card) {q : ι → 𝕜} (hq : InBox s (↑s.card * μ) q) (hvertex : AtMostOneInteriorCoord s q) : bernExp s q g < bernExp s (fun (x : ι) => μ) g

The vertex reading fails in general, not just at one witness. For g strictly grid-convex, Theorem 3 says the unique maximiser over the fixed-mean box is the constant vector p ≡ μ; when 0 < μ < 1 every one of its #s coordinates is interior, so for #s ≥ 2 no vertex can dominate it.

Existence of the extremum over ℝ — the compactness input, discharged

def MiscMath.Probability.suppBox {ι : Type u_1} [DecidableEq ι] (s : Finset ι) : Set (ι → ℝ)

The supported box: coordinates off s are pinned at 0. The box {p | InBox s lam p} itself is closed but not bounded — coordinates off s are unconstrained — so the compactness argument runs here instead, and bernExp_congr says bernExp cannot tell the difference.

Equations

• MiscMath.Probability.suppBox s = Set.univ.pi fun (i : ι) => if i ∈ s then Set.Icc 0 1 else {0}

theorem MiscMath.Probability.isCompact_suppBox {ι : Type u_1} [DecidableEq ι] (s : Finset ι) : IsCompact (suppBox s)

Tychonoff: the supported box is compact. No Fintype ι is needed.

theorem MiscMath.Probability.continuous_bernExp {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (g : ℕ → ℝ) : Continuous fun (p : ι → ℝ) => bernExp s p g

bernExp is continuous in p over ℝ.

theorem MiscMath.Probability.isClosed_meanSlice {ι : Type u_1} (s : Finset ι) (lam : ℝ) : IsClosed {p : ι → ℝ | ∑ i ∈ s, p i = lam}

The mean slice is closed.

def MiscMath.Probability.trunc {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (p : ι → ℝ) : ι → ℝ

The truncation of p to s.

Equations

• MiscMath.Probability.trunc s p i = if i ∈ s then p i else 0

theorem MiscMath.Probability.trunc_agrees {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (p : ι → ℝ) (i : ι) : i ∈ s → p i = trunc s p i

theorem MiscMath.Probability.bernExp_trunc {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (p : ι → ℝ) (g : ℕ → ℝ) : bernExp s (trunc s p) g = bernExp s p g

theorem MiscMath.Probability.trunc_mem_suppBox {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {lam : ℝ} {p : ι → ℝ} (hp : InBox s lam p) : trunc s p ∈ suppBox s ∩ {q : ι → ℝ | ∑ i ∈ s, q i = lam}

theorem MiscMath.Probability.inBox_of_mem_suppBox {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {lam : ℝ} {q : ι → ℝ} (hq : q ∈ suppBox s ∩ {r : ι → ℝ | ∑ i ∈ s, r i = lam}) : InBox s lam q

theorem MiscMath.Probability.exists_isMaxOn_bernExp {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {lam : ℝ} (g : ℕ → ℝ) {p₀ : ι → ℝ} (hp₀ : InBox s lam p₀) : ∃ (q : ι → ℝ), InBox s lam q ∧ ∀ (r : ι → ℝ), InBox s lam r → bernExp s r g ≤ bernExp s q g

Existence of a maximiser over ℝ, as soon as the box is nonempty. Only the supported box is compact, which is why bernExp_congr is needed.

theorem MiscMath.Probability.exists_isMinOn_bernExp {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {lam : ℝ} (g : ℕ → ℝ) {p₀ : ι → ℝ} (hp₀ : InBox s lam p₀) : ∃ (q : ι → ℝ), InBox s lam q ∧ ∀ (r : ι → ℝ), InBox s lam r → bernExp s q g ≤ bernExp s r g

Existence of a minimiser, by negating g.

theorem MiscMath.Probability.hoeffding_cor21 {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {lam : ℝ} (g : ℕ → ℝ) {p : ι → ℝ} (hp : InBox s lam p) : ∃ (q : ι → ℝ), InBox s lam q ∧ AtMostOneInteriorValue s q ∧ ∀ (r : ι → ℝ), InBox s lam r → bernExp s r g ≤ bernExp s q g

Hoeffding (1956), Corollary 2.1, over ℝ with no hypotheses at all beyond membership in the fixed-mean box: the maximum of bernExp s · g is attained at a point whose coordinates take at most the three values {0, x, 1}. g is arbitrary — no convexity, no monotonicity.

theorem MiscMath.Probability.hoeffding_cor21_min {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {lam : ℝ} (g : ℕ → ℝ) {p : ι → ℝ} (hp : InBox s lam p) : ∃ (q : ι → ℝ), InBox s lam q ∧ AtMostOneInteriorValue s q ∧ ∀ (r : ι → ℝ), InBox s lam r → bernExp s q g ≤ bernExp s r g

The minimum direction of the same.

The shape data

At a point with at most one interior value the coordinates take only 0, 1 and one repeated value x. Counting them gives (a, b, r) and the mean equation a + r·x = lam, so the extremal candidates are indexed by the pair (a, b) alone — at most (#s + 1)² of them.

theorem MiscMath.Probability.box_trichotomy {ι : Type u_1} {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] {s : Finset ι} {lam : 𝕜} {q : ι → 𝕜} (hq : InBox s lam q) {i : ι} (hi : i ∈ s) : q i = 1 ∨ q i = 0 ∨ i ∈ interiorCoords s q

The three-way partition of the box at a point: ones, zeros, interior.

theorem MiscMath.Probability.shape_of_atMostOneInteriorValue {ι : Type u_1} {𝕜 : Type u_2} [CommRing 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Finset ι} {lam : 𝕜} {q : ι → 𝕜} (hq : InBox s lam q) (hshape : AtMostOneInteriorValue s q) : ∃ (x : 𝕜), (∀ i ∈ interiorCoords s q, q i = x) ∧ {i ∈ s | q i = 1}.card + {i ∈ s | q i = 0}.card + (interiorCoords s q).card = s.card ∧ ↑{i ∈ s | q i = 1}.card + ↑(interiorCoords s q).card * x = lam

The shape data and the mean equation. Every point of the box with at most one interior value is described by a coordinates at 1, b at 0, and r = #s - a - b at a common x, with a + r·x = lam.

The vertex reading, refuted concretely

The general refutation is vertex_reduction_fails_of_strictConvex. The rational instance below is the same statement made concrete and machine-checked, and it also exhibits the correct form holding at the same point.

def MiscMath.Probability.VertexReduction : Prop

The reduction with the vertex conclusion: every point of the box is dominated by one with at most one interior coordinate.

Equations

• One or more equations did not get rendered due to their size.

def MiscMath.Probability.VertexReductionMin : Prop

The same, for the minimum.

Equations

• One or more equations did not get rendered due to their size.

def MiscMath.Probability.gMax : ℕ → ℚ

g = (1,0,1): strictly grid-convex, secondDiff g 0 = 2 > 0.

Equations

• MiscMath.Probability.gMax k = if k = 1 then 0 else 1

def MiscMath.Probability.gMin : ℕ → ℚ

g = (0,1,0) — the witness for the minimum.

Equations

• MiscMath.Probability.gMin k = if k = 1 then 1 else 0

def MiscMath.Probability.exHalf : ℕ → ℚ

The witness point p = (1/2, 1/2) on s = {0,1} with lam = 1.

Equations

• MiscMath.Probability.exHalf x✝ = 1 / 2

theorem MiscMath.Probability.exHalf_inBox : InBox {0, 1} 1 exHalf

theorem MiscMath.Probability.bernExp_two (q g : ℕ → ℚ) (hq : q 0 + q 1 = 1) : bernExp {0, 1} q g = g 1 + q 0 * q 1 * (g 0 - 2 * g 1 + g 2)

On s = {0,1} the value is g 1 + (pair product)·secondDiff g 0.

theorem MiscMath.Probability.exHalf_value : bernExp {0, 1} exHalf gMax = 1 / 2

theorem MiscMath.Probability.exHalf_isMax (r : ℕ → ℚ) : InBox {0, 1} 1 r → bernExp {0, 1} r gMax ≤ bernExp {0, 1} exHalf gMax

The witness point really is the maximiser: 2τ(1-τ) ≤ 1/2.

theorem MiscMath.Probability.two_le_interior_card {q : ℕ → ℚ} (h0 : 0 ∈ interiorCoords {0, 1} q) (h1 : 1 ∈ interiorCoords {0, 1} q) : 2 ≤ (interiorCoords {0, 1} q).card

On s = {0,1} two interior coordinates already break the vertex clause.

theorem MiscMath.Probability.exHalf_unique_max (r : ℕ → ℚ) : InBox {0, 1} 1 r → bernExp {0, 1} r gMax = 1 / 2 → r 0 = 1 / 2 ∧ r 1 = 1 / 2

… uniquely: 2τ(1-τ) = 1/2 forces τ = 1/2.

theorem MiscMath.Probability.exHalf_not_vertex : ¬AtMostOneInteriorCoord {0, 1} exHalf

… and it has two interior coordinates, so it is not a vertex.

theorem MiscMath.Probability.exHalf_atMostOneInteriorValue : AtMostOneInteriorValue {0, 1} exHalf

… while Hoeffding's own shape does hold there: one interior value at two coordinates. This is the whole distinction, in one witness.

theorem MiscMath.Probability.vertex_two {q : ℕ → ℚ} (hq : InBox {0, 1} 1 q) (hv : AtMostOneInteriorCoord {0, 1} q) : q 0 * q 1 = 0

On the box {p | p 0 + p 1 = 1} a vertex is (1,0) or (0,1).

theorem MiscMath.Probability.vertex_reduction_false : ¬VertexReduction

The vertex reading of Corollary 2.1 is FALSE (maximum direction). At s = {0,1}, lam = 1, g = (1,0,1): the maximum 1/2 is attained only at (1/2,1/2), while every vertex of the box gives 0.

theorem MiscMath.Probability.vertex_reduction_min_false : ¬VertexReductionMin

… and in the minimum direction too, with g = (0,1,0): the minimum 1/2 is attained only at (1/2,1/2), every vertex gives 1.