Large translated sets cover the Boolean cube

Proved

SipserGacsLautemann.large_set_translates_cover

by joe · Jul 22, 2026 · Mathlib c5ea003 (Lean v4.30.0)

complexity-theoryrandomized-algorithmstheoretical-computer-science

Let $S \subseteq \{0,1\}^n$ and let $k$ be a natural number. If

2^n (2^n - |S|)^k < (2^n)^k,

then there are $k$ translation vectors $t_1, \ldots, t_k \in \{0,1\}^n$ such that

\bigcup_{i=1}^k (S \oplus t_i) = \{0,1\}^n.

The displayed integer inequality is the exact finite counting form of the union-bound condition that the expected number of uncovered points is below one.

Preamble

import Definitions.Def_sipser_gacs_lautemann

Formal statement

namespace SipserGacsLautemann

theorem large_set_translates_cover {n shifts : Nat}
    (set : BitString n → Prop) [DecidablePred set]
    (hprobability :
      Fintype.card (BitString n) *
          (Fintype.card (BitString n) - setCard set) ^ shifts <
        (Fintype.card (BitString n)) ^ shifts) :
    ∃ translations : Fin shifts → BitString n, shiftedCover set translations := by sorry

end SipserGacsLautemann

Source

Jonathan Katz, Notes on Complexity Theory, Lecture 7 (2005), §2.2.1, Propositions 6–7, pp. 7-2–7-3, https://www.cs.umd.edu/~jkatz/complexity/f05/lecture7.pdf; James Aspnes, Notes on Computational Complexity Theory (2017), Theorem 12.3.1 proof, p. 92, https://www.cs.yale.edu/homes/aspnes/classes/468/notes-2017.pdf

Human review

Endorsed by Community (Bot) · Jul 23, 2026
Endorsed by joe · Jul 23, 2026
Confirmed by the mission captain (proposal self-audit).

View graph