Few indices are far above the average

Let f be a function with natural numbers as values on a nonempty finite set Q. Division is avoided: "f p is at most k times the average of f" is written f p * |Q| ≤ k * ∑ p' ∈ Q, f p'.

• Fewer than |Q|/k indices are more than k times as bad as the average (Finset.mul_card_above_average_lt, Markov's inequality).
• So for k functions there is one index at which each of them is at most k times its average (Finset.exists_forall_mul_card_le_mul_sum, the union bound).
• Given a vertex map v : I → V, nonnegative payoffs W : I → α → R, and vertex-wise sub-probability weights p : V → α → R (0 ≤ p u a and ∑ a, p u a ≤ 1), choosing the best label at each vertex produces a deterministic assignment f : V → α whose total payoff is at least the weighted payoff (Finset.exists_choice_sum_le).

For the non-strict, unnormalised finite Markov bound, see Finset.mul_card_filter_le_sum in Complexity/Foundations/Data/Finset/Markov.lean.

Adapted from Average.lean in anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5.

Main results

• Finset.exists_forall_mul_card_le_mul_sum: simultaneous finite average bound.
• Finset.exists_choice_sum_le: deterministic vertex-wise maximum choice beats any vertex-wise sub-probability weighting.

theorem Finset.mul_card_above_average_lt {ι : Type u_1} {Q : Finset ι} (hQ : Q.Nonempty) (k : ℕ) (f : ι → ℕ) : k * {p ∈ Q | k * ∑ p' ∈ Q, f p' < f p * Q.card}.card < Q.card

Markov's inequality: fewer than |Q|/k indices are more than k times as bad as the average.

theorem Finset.exists_forall_mul_card_le_mul_sum {ι : Type u_1} {Q : Finset ι} (hQ : Q.Nonempty) (k : ℕ) (f : Fin k → ι → ℕ) : ∃ p ∈ Q, ∀ (i : Fin k), f i p * Q.card ≤ k * ∑ p' ∈ Q, f i p'

The union bound: one index is good for k functions at once, in that each function is at most k times its average there.

theorem Finset.exists_choice_sum_le {I : Type u_1} {V : Type u_2} {α : Type u_3} {R : Type u_4} [Fintype I] [Fintype α] [Nonempty α] [CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R] (v : I → V) (W : I → α → R) (hW : ∀ (i : I) (a : α), 0 ≤ W i a) (p : V → α → R) (hp0 : ∀ (u : V) (a : α), 0 ≤ p u a) (hp1 : ∀ (u : V), ∑ a : α, p u a ≤ 1) : ∃ (f : V → α), ∑ i : I, ∑ a : α, p (v i) a * W i a ≤ ∑ i : I, W i (f (v i))

Deterministic vertex-choice lemma: given a vertex map v : I → V, nonnegative payoffs W : I → α → R, and vertex-wise sub-probability weights p : V → α → R (0 ≤ p u a and ∑ a, p u a ≤ 1), choosing the best label at each vertex produces a deterministic assignment f : V → α whose payoff is at least the weighted payoff under p.