Probabilistic combinatorics

Probabilistic methods and random discrete structures outside random graphs: the Lovász local lemma, Littlewood–Offord and Tomaszewski anti-concentration for signed sums, concentration of subset sums, the isolation lemma, thresholds and expectation thresholds, random k-SAT thresholds, perfect matchings in random hypergraphs, the Chvátal–Sankoff constant for longest common subsequences, and moment-based counting bounds.

TheoremIsolation lemma#✓fully proved

Let \(n \ge 1\) and let \(\mathcal{F}\) be a nonempty family of subsets of \(\{0, 1, \dots, n - 1\}\). Assign each element \(i\) a weight \(w(i) \in \{1, 2, \dots, 2n\}\) and give a set \(S\) the weight \(w(S) = \sum_{i \in S} w(i)\). Then, among all \((2n)^n\) weight functions \(w\), the fraction for which exactly one member of \(\mathcal{F}\) has minimum weight is at least \(1/2\).

Equivalently, if the weights are chosen independently and uniformly at random, the minimum-weight member of \(\mathcal{F}\) is unique with probability at least \(1/2\).

theorem isolation_lemma {n : ℕ} (hn : 0 < n)
    (F : Finset (Finset (Fin n))) (hF : F.Nonempty) :
    (((Finset.univ.filter (fun w : Fin n → Fin (2 * n) =>
      (F.filter (fun S => ∀ T ∈ F,
        ∑ i ∈ S, ((w i).val + 1) ≤ ∑ i ∈ T, ((w i).val + 1))).card = 1)).card : ℚ)
      / (Fintype.card (Fin n → Fin (2 * n)) : ℚ)) ≥ 1 / 2
Sources
  • https://en.wikipedia.org/wiki/Isolation_lemma

TheoremSymmetric Lovász Local Lemma#✓fully proved

Let \(\Omega\) be a finite set with a probability mass function \(P\), that is, \(P(\omega) \ge 0\) for every \(\omega \in \Omega\) and \(\sum_{\omega \in \Omega} P(\omega) = 1\), and write \(\Pr[E] = \sum_{\omega \in E} P(\omega)\) for \(E \subseteq \Omega\). Let \((A_i)_{i \in I}\) be a family of events indexed by a finite set \(I\), let \(G\) be a simple graph on \(I\) whose maximum degree is at most a natural number \(d\), and let \(p \ge 0\) be a real number. Suppose that \(\Pr[A_i] \le p\) for every \(i \in I\), and that for every \(i \in I\) and every set \(S \subseteq I\) containing neither \(i\) nor any neighbour of \(i\) in \(G\), \(\Pr[A_i \cap \bigcap_{j \in S} A_j] = \Pr[A_i] \cdot \Pr[\bigcap_{j \in S} A_j]\). If \(e \cdot p \cdot (d + 1) \le 1\), then \(\Pr[\bigcap_{i \in I} (\Omega \setminus A_i)] > 0\), that is, with positive probability none of the events \(A_i\) occurs.

The independence hypothesis, taken over all such \(S\) (including \(S = \emptyset\)), says that each \(A_i\) is mutually independent of the family of events \(A_j\) with \(j\) neither \(i\) nor a neighbour of \(i\).

MathlibExt.Probability.Combinatorics.LovaszLocalLemma.lovasz_local_lemma_symmetric_finite · 20 lines 
theorem lovasz_local_lemma_symmetric_finite
    [Fintype Ω] [Fintype I] [DecidableEq I]
    (pmf : Ω → ℝ)
    (hpmf_nonneg : ∀ ω, 0 ≤ pmf ω)
    (hpmf_sum : ∑ ω : Ω, pmf ω = 1)
    (A : I → Set Ω)
    (G : SimpleGraph I) [DecidableRel G.Adj]
    (p : ℝ) (d : ℕ)
    (hp_nonneg : 0 ≤ p)
    (hmaxDeg : G.maxDegree ≤ d)
    (hp_le : ∀ i : I,
      ∑ ω : Ω, (if ω ∈ A i then pmf ω else 0) ≤ p)
    (hDep : ∀ (i : I) (S : Finset I),
      (∀ j ∈ S, j ∉ insert i (G.neighborSet i)) →
      ∑ ω : Ω,
        (if ω ∈ A i ∧ ∀ j ∈ S, ω ∈ A j then pmf ω else 0) =
      (∑ ω : Ω, (if ω ∈ A i then pmf ω else 0)) *
      (∑ ω : Ω, (if ∀ j ∈ S, ω ∈ A j then pmf ω else 0)))
    (hExp : Real.exp 1 * p * ((d : ℝ) + 1) ≤ 1) :
    0 < ∑ ω : Ω, (if ∀ i : I, ω ∉ A i then pmf ω else 0)
Sources
  • N. Alon and J. H. Spencer, The Probabilistic Method, third edition, Wiley, 2008, Corollary 5.1.2, for the criterion \(e p (d + 1) \le 1\); the original local lemma of P. Erdős and L. Lovász (1975) gives the earlier weaker criterion \(4 p d \le 1\).
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.