The Lovász Local Lemma #
Let A i be finitely many events in a probability space, and let Γ i be a set of indices such
that A i is (lopsidedly) independent of the events outside Γ i ∪ {i}: for every set s of
indices avoiding Γ i and i, the probability that A i occurs while no A j with j ∈ s
occurs is at most μ (A i) times the probability that no A j with j ∈ s occurs. This holds
with equality when A i is mutually independent of the events A j with j ∉ Γ i ∪ {i}, so Γ
may be the neighborhood map of a dependency graph Alon and Spencer, Section 5.1;
the inequality is the lopsided condition of Erdős and Spencer [ES91].
- Asymmetric form (
Cslib.Probability.prod_one_sub_le_measureReal_iInter_compl): ifx i ∈ [0, 1]andμ (A i) ≤ x i ∏ j ∈ Γ i, (1 - x j)for everyi, then no event occurs with probability at least∏ i, (1 - x i)Alon and Spencer, Lemma 5.1.1. - Symmetric form (
Cslib.Probability.measureReal_iInter_compl_pos): if every event has probability at mostq, everyΓ ihas at mostdelements ande q (d + 1) ≤ 1, then with positive probability no event occurs Alon and Spencer, Corollary 5.1.2, [EL75]; quantitatively, with probability at least(d / (d + 1)) ^ nfornevents (Cslib.Probability.pow_le_measureReal_iInter_compl).
The proof shows, by strong induction on s, that μ (A i ∩ ⋂ j ∈ s, (A j)ᶜ) is at most
x i * μ (⋂ j ∈ s, (A j)ᶜ) for i ∉ s; no conditional probabilities or divisions appear.
In a finite product space Cslib.Probability.PMF.pi p, events depending on disjoint sets of
coordinates (Mathlib's DependsOn) are independent
(Cslib.Probability.PMF.toOuterMeasure_pi_inter_eq_mul, the PMF form of
ProbabilityTheory.indepSet_pi_of_dependsOn). So if each event A i depends only on the
coordinates in a set vbl i, the events sharing no coordinate
with A i satisfy the hypothesis, giving the variable version of the local lemma used for
satisfiability and coloring problems (Cslib.Probability.PMF.prod_one_sub_le_pi_iInter_compl,
Cslib.Probability.PMF.pi_iInter_compl_pos) [MT10].
Main results #
Cslib.Probability.prod_one_sub_le_measureReal_iInter_compl: the asymmetric (lopsided) local lemma for a probability measure.Cslib.Probability.pow_le_measureReal_iInter_compl,Cslib.Probability.measureReal_iInter_compl_pos: the symmetric local lemma.Cslib.Probability.PMF.toOuterMeasure_pi_inter_eq_mul: events on disjoint coordinates of a product are independent.Cslib.Probability.PMF.prod_one_sub_le_pi_iInter_compl,Cslib.Probability.PMF.pi_iInter_compl_pos: the asymmetric and symmetric local lemmas for events depending on sets of independent coordinates.
References #
- N. Alon, J. H. Spencer, The Probabilistic Method, Chapter 5
- P. Erdős, L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions
- P. Erdős, J. Spencer, Lopsided Lovász Local Lemma and Latin transversals
- [R. A. Moser, G. Tardos, A constructive proof of the general Lovász Local Lemma] [MT10]
The Lovász Local Lemma, asymmetric and lopsided form [Alon and Spencer, Lemma 5.1.1]
[AS16], [ES91]: let A i be finitely many measurable events and let Γ i
be sets of indices such that A i is lopsidedly independent of the events outside Γ i ∪ {i}.
If x i ∈ [0, 1] and μ (A i) ≤ x i ∏ j ∈ Γ i, (1 - x j) for every i, then no event occurs with
probability at least ∏ i, (1 - x i), which is positive when every x i < 1.
The symmetric Lovász Local Lemma, quantitative form: if each of n measurable events has
probability at most q, each A i is lopsidedly independent of the events outside Γ i ∪ {i},
each Γ i has at most d elements, and e q (d + 1) ≤ 1, then no event occurs with probability
at least (d / (d + 1)) ^ n. This is positive when d ≥ 1.
The symmetric Lovász Local Lemma Alon and Spencer, Corollary 5.1.2,
[EL75]: if each of finitely many measurable events has probability at most q, each
A i is lopsidedly independent of the events outside Γ i ∪ {i}, each Γ i has at most d
elements, and e q (d + 1) ≤ 1, then with positive probability no event occurs.
Events on disjoint coordinates are independent: in an independent product, an event
depending only on the coordinates in S and an event depending only on the coordinates in a
disjoint set T are independent. This is the finite-PMF form of
ProbabilityTheory.indepSet_pi_of_dependsOn.
The Lovász Local Lemma for independent coordinates, asymmetric form: let each event A i
of an independent product depend only on the coordinates in vbl i, and let Γ i contain every
other index whose event shares a coordinate with A i. If x i ∈ [0, 1] and
Pr[A i] ≤ x i ∏ j ∈ Γ i, (1 - x j) for every i, then no event occurs with probability at least
∏ i, (1 - x i).
The symmetric Lovász Local Lemma for independent coordinates: let each event A i of an
independent product depend only on the coordinates in vbl i, let each event share coordinates
with at most d other events, and let each event have probability at most q. If
e q (d + 1) ≤ 1, then with positive probability no event occurs.