Plurality over a finite set

The pigeonhole fact behind every "decode a cloud by majority vote" step: among the Fintype.card α possible labels, some label is worn by at least a 1 / Fintype.card α fraction of a finite set.

Dinur's degree reduction uses this to decode the blown-up assignment — a vertex is given the label that the most half-edges of its cloud claim — and the bound below is exactly what makes the disagreeing part of a cloud small enough for the cloud expander to charge it.

Main results

• Complexity.exists_plurality — some label captures at least 1 / card α of the set

theorem Complexity.exists_plurality {β α : Type} [DecidableEq α] [Fintype α] [Nonempty α] (S : Finset β) (A : β → α) : ∃ (a : α), S.card ≤ Fintype.card α * {p ∈ S | A p = a}.card

Plurality. Some label is taken by at least a 1 / Fintype.card α fraction of S.