Documentation

Atlas.ProbabilisticMethodsInCombinatorics.code.Chapter6.LovaszLocalLemma

def LovaszLocalLemma.IndepOfEvents {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (A₀ : Set Ω) (A : ιSet Ω) (S : Finset ι) (μ : MeasureTheory.Measure Ω := by volume_tac) :

The event $A_0$ is mutually independent (under $\mu$) of all sign choices of the events $A_i$ for $i \in S$: for every assignment of each $B_i$ to either $A_i$ or $A_i^c$, $\mu(A_0 \cap \bigcap_{i \in S} B_i) = \mu(A_0)\,\mu(\bigcap_{i \in S} B_i)$.

Instances For
    def LovaszLocalLemma.IsDependencyDigraph {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [DecidableEq ι] (G : Digraph ι) [DecidableRel G.Adj] (A : ιSet Ω) (μ : MeasureTheory.Measure Ω := by volume_tac) :

    A directed graph $G$ is a dependency digraph for the family $(A_i)_{i \in \iota}$ if, for every $i$ and every finite set $S$ of indices distinct from $i$ and not adjacent to $i$ in $G$, the event $A_i$ is mutually independent of the events $\{A_j\}_{j \in S}$.

    Instances For
      def LovaszLocalLemma.neighbors {ι : Type u_2} [Fintype ι] [DecidableEq ι] (G : Digraph ι) [DecidableRel G.Adj] (i : ι) :

      The out-neighborhood of $i$ in the digraph $G$, viewed as a finite set.

      Instances For
        theorem LovaszLocalLemma.relative_product_bound_bounded {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [DecidableEq ι] (A : ιSet Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hA : ∀ (i : ι), MeasurableSet (A i)) (x : ι) (hx01 : ∀ (i : ι), 0 x i x i < 1) (n : ) (hcond : ∀ (T : Finset ι), T.card < niT, μ (A i jT, (A j)) ENNReal.ofReal (x i) * μ (⋂ jT, (A j))) (S₁ S₂ : Finset ι) (hdisj : Disjoint S₁ S₂) (hcard : (S₁ S₂).card n) :
        μ (⋂ jS₁ S₂, (A j)) ENNReal.ofReal (∏ jS₁, (1 - x j)) * μ (⋂ jS₂, (A j))

        Inductive bound built from hcond: given a uniform conditional estimate up to size $n$, the probability of avoiding all events in $S_1 \cup S_2$ is at least $\bigl(\prod_{j \in S_1}(1 - x_j)\bigr) \cdot \mu(\bigcap_{j \in S_2} A_j^c)$ whenever $S_1, S_2$ are disjoint and $|S_1 \cup S_2| \le n$.

        theorem LovaszLocalLemma.cond_prob_bound {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [DecidableEq ι] (G : Digraph ι) [DecidableRel G.Adj] (A : ιSet Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hA : ∀ (i : ι), MeasurableSet (A i)) (hG : IsDependencyDigraph G A μ) (x : ι) (hx01 : ∀ (i : ι), 0 x i x i < 1) (hbound : ∀ (i : ι), μ (A i) ENNReal.ofReal (x i * jneighbors G i, (1 - x j))) (S : Finset ι) (i : ι) (hiS : iS) :
        μ (A i jS, (A j)) ENNReal.ofReal (x i) * μ (⋂ jS, (A j))

        The induction underlying the general Lovász Local Lemma: under the dependency-digraph hypothesis hG and the bound $\mu(A_i) \le x_i \prod_{j \in N(i)}(1 - x_j)$, for every finite $S$ not containing $i$ we have $\mu(A_i \cap \bigcap_{j \in S} A_j^c) \le x_i \, \mu(\bigcap_{j \in S} A_j^c)$.

        theorem LovaszLocalLemma.lovasz_local_lemma_general {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [DecidableEq ι] (G : Digraph ι) [DecidableRel G.Adj] (A : ιSet Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hA : ∀ (i : ι), MeasurableSet (A i)) (hG : IsDependencyDigraph G A μ) (x : ι) (hx01 : ∀ (i : ι), 0 x i x i < 1) (hbound : ∀ (i : ι), μ (A i) ENNReal.ofReal (x i * jneighbors G i, (1 - x j))) :
        μ (⋂ (i : ι), (A i)) ENNReal.ofReal (∏ i : ι, (1 - x i))

        General Lovász Local Lemma (Theorem 6.1.9): given events $A_i$ with dependency digraph $G$ and weights $x_i \in [0,1)$ such that $\mu(A_i) \le x_i \prod_{j \in N(i)}(1 - x_j)$ for every $i$, one has $\mu(\bigcap_i \overline{A_i}) \ge \prod_i (1 - x_i)$, so in particular it is positive.

        theorem LovaszLocalLemma.prod_one_sub_ge_one_sub_sum {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (f : ι) (hf0 : is, 0 f i) (hf1 : is, f i 1) :
        1 - is, f i is, (1 - f i)

        Weierstrass-style inequality: for $f_i \in [0,1]$ on a finite set $s$, $1 - \sum_{i \in s} f_i \le \prod_{i \in s} (1 - f_i)$.

        theorem LovaszLocalLemma.lovasz_local_lemma_cor_6_1_10 {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [DecidableEq ι] (G : Digraph ι) [DecidableRel G.Adj] (A : ιSet Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hA : ∀ (i : ι), MeasurableSet (A i)) (hG : IsDependencyDigraph G A μ) (p : ι) (hp_nn : ∀ (i : ι), 0 p i) (hp_lt : ∀ (i : ι), p i < 1 / 2) (hp_bound : ∀ (i : ι), μ (A i) ENNReal.ofReal (p i)) (hp_sum : ∀ (i : ι), jneighbors G i, p j 1 / 4) :
        μ (⋂ (i : ι), (A i)) > 0

        Corollary 6.1.10 of LLL: if every $p_i < 1/2$ and for every $i$ the sum $\sum_{j \in N(i)} p_j \le 1/4$, then $\mu(\bigcap_i \overline{A_i}) > 0$.

        theorem LovaszLocalLemma.one_sub_inv_pow_ge_inv_exp (d : ) (hd : 1 d) :
        (1 - 1 / (d + 1)) ^ d 1 / Real.exp 1

        Real-analytic helper inequality $(1 - 1/(d+1))^d \ge 1/e$ for $d \ge 1$, used in the symmetric LLL.

        theorem LovaszLocalLemma.lovasz_local_lemma_symmetric {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [DecidableEq ι] (G : Digraph ι) [DecidableRel G.Adj] (A : ιSet Ω) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hA : ∀ (i : ι), MeasurableSet (A i)) (hG : IsDependencyDigraph G A μ) {p : } {d : } (hp : 0 p) (hd : 1 d) (hprob : ∀ (i : ι), μ (A i) ENNReal.ofReal p) (hdeg : ∀ (i : ι), (neighbors G i).card d) (hcond : Real.exp 1 * p * (d + 1) 1) :
        μ (⋂ (i : ι), (A i)) > 0

        Symmetric Lovász Local Lemma (Theorem 6.1.7): if each event satisfies $\mu(A_i) \le p$, the dependency digraph has maximum out-degree at most $d \ge 1$, and $e p (d+1) \le 1$, then $\mu(\bigcap_i \overline{A_i}) > 0$.