Erdős–Lovász local lemma, symmetric form, uniform finite probability space (Theorem 1)

Let $\Omega$ be a finite nonempty set with the uniform probability $\Pr(A) = |A| / |\Omega|$ on its subsets. Let $A_1, \dots, A_n \subseteq \Omega$ be events, thought of as the good events, and let $\Gamma(1), \dots, \Gamma(n) \subseteq \{1, \dots, n\}$ form a dependency graph: for every $i$ and every set $S$ of indices with $i \notin S$ and $S \cap \Gamma(i) = \emptyset$, $\Pr\big(A_i \cap \bigcap_{j \in S} A_j\big) = \Pr(A_i) \Pr\big(\bigcap_{j \in S} A_j\big)$.

Suppose every $\Gamma(i)$ has at most $d$ elements, $\Pr(A_i) \ge 1 - p$ for every $i$, and $p \cdot e \cdot (d + 1) \le 1$. Then

so some outcome lies in every good event.

This is the symmetric local lemma of Erdős and Lovász, Theorem 1 in Ambainis, Kempe and Sattath, obtained as the classical instance of the abstract lemma QLLL.Valuation.lll_symmetric. Other formulations exist on the platform, for example AppliedComb.ManyFaces.local_lemma_symmetric and Combinatorics.finite_symmetric_local_lemma.

Formalization Note The paper states the classical lemma for bad events $B_i$ on an arbitrary probability space. Here it is stated for the good events $A_i = B_i^{c}$ under the uniform probability on a finite set, and the dependency hypothesis is independence of $A_i$ from intersections of good events. Under the usual notion of mutual independence (from the $\sigma$-algebra generated by the non-neighbours) this hypothesis is implied, so the usual applications are covered.