Short ε-biased lists exist

A list s₁, …, s_d of bit strings in ι → Bool is ε-biased when the uniform distribution over the list is ε-biased (Cslib.BitString.IsSmallBias): for every nonempty set S of coordinates, |Σⱼ χ_S(sⱼ)| ≤ ε d. If ε ≥ 0, d ≥ 1 and 2 · 2^|ι| · exp(-ε² d / 2) < 1, such a list exists (Cslib.BitString.exists_isSmallBias_map_of_exp_lt). Unlike the explicit powering construction (Cslib.BitString.exists_isSmallBias_uniformOfFintype_map), whose lists have length a power of four, this gives every length d for which the bound holds, as [OAI26c] needs for its prescribed number of shifts.

The proof is the probabilistic method in counting form. For a fixed nonempty S the parities on S of the d strings are d independent unbiased bits: a shear of the cube (shear), adding to one coordinate i₀ ∈ S of each string the parity on S \ {i₀}, turns them into d coordinates of a uniformly random bit string. Hoeffding's inequality (Cslib.BitString.card_filter_le_abs_card_filter_sub_half_le) then bounds the number of lists biased at S by a 2 exp(-ε² d / 2) fraction (Cslib.BitString.card_biased_le), and a union bound over the fewer than 2^|ι| nonempty sets leaves an ε-biased list. This is the existence argument for the ε-biased shifts in [OpenAI2026ETH, proof of Lemma 6.1, (6.2)]; such lists are the generators of small-bias Cayley graphs Naor and Naor.

Main results

• Cslib.BitString.sum_chi_eq: the sum of a character over a list counts the odd parities.
• Cslib.BitString.card_biased_le: few lists are biased at a fixed nonempty set.
• Cslib.BitString.exists_isSmallBias_map_of_exp_lt: short ε-biased lists exist.

References

• OpenAI, The Exponential Time Hypothesis is False, §6.1
• J. Naor, M. Naor, Small-bias probability spaces

theorem Cslib.BitString.sum_chi_eq {ι : Type u_1} {d : ℕ} (S : Finset ι) (s : Fin d → ι → Bool) : ∑ j : Fin d, chi ℝ S (s j) = ↑d - 2 * ↑{j : Fin d | parityOn S (s j) = true}.card

The sum of the character of S over a list is d minus twice the number of strings of the list with odd parity on S.

theorem Cslib.BitString.card_biased_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {d : ℕ} {S : Finset ι} (hS : S.Nonempty) {ε : ℝ} (hε : 0 ≤ ε) : ↑{s : Fin d → ι → Bool | ε * ↑d ≤ |∑ j : Fin d, chi ℝ S (s j)|}.card ≤ 2 * 2 ^ (d * Fintype.card ι) * Real.exp (-(ε ^ 2 * ↑d / 2))

Few lists are biased at a fixed nonempty set: at most a 2 exp(-ε² d / 2) fraction of the lists of d bit strings have |Σⱼ χ_S(sⱼ)| ≥ ε d.

theorem Cslib.BitString.exists_isSmallBias_map_of_exp_lt {ι : Type u_1} [Fintype ι] [DecidableEq ι] {d : ℕ} [NeZero d] {ε : ℝ} (hε : 0 ≤ ε) (h : 2 * 2 ^ Fintype.card ι * Real.exp (-(ε ^ 2 * ↑d / 2)) < 1) : ∃ (s : Fin d → ι → Bool), IsSmallBias ε (PMF.map s (Probability.PMF.uniformOfFintype (Fin d)))

Short ε-biased lists exist: if ε ≥ 0 and 2 · 2^|ι| · exp(-ε² d / 2) < 1, some list of d ≥ 1 bit strings has, at every nonempty set S, |Σⱼ χ_S(sⱼ)| < ε d; so the uniform distribution over it is ε-biased.