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

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)$.

Let $y_1, \dots, y_n$ be real numbers with $0 \le y_i < 1$ such that $\Pr(A_i) \ge 1 - y_i \prod_{j \in \Gamma(i)} (1 - y_j)$ for every $i$. Then

This is the asymmetric local lemma of Erdős and Lovász, Theorem 13 in Ambainis, Kempe and Sattath, obtained as the classical instance of the abstract lemma QLLL.Valuation.lll at uniform probability. Other formulations of the classical local lemma exist on the platform, for example AppliedComb.ManyFaces.local_lemma_asymmetric 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.