The asymmetric Lovász local lemma #
Mathlib does not contain the Lovász local lemma, so we prove the version we need from
scratch, for the finite counting probability space of BSLambda.LLL.Prob.
Events are given by a family Ev : I → Finset (Cfg β), each Ev i being determined by the
coordinate set supp i. Two events are dependent when their supports meet. nbr supp i
collects the indices of the events other than i that are dependent with Ev i.
The main results are pr_avoid_pos (the general asymmetric local lemma of Section 10 of
bs_lambda.txt) and pr_avoid_pos_two_type (the two-type statement of Section 10.2).
The last section is independent of the local lemma: pr_le_prod_of_pinned and its
constant-alphabet form pr_le_pow_of_pinned bound the probability of an event that pins a set
of coordinates to targets read off a disjoint set of coordinates. They supply the hypothesis
hcond above at the places where the local lemma is applied.
Adapted for Lean Pool from Timeroot/BS_Lam at commit
7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.
Dependency neighbourhoods and avoidance events #
The dependency neighbourhood: other events whose supports meet ours.
Instances For
Membership in the dependency neighbourhood.
The events indexed outside the dependency neighbourhood of i are supported away from
supp i.
The event that none of the bad events indexed by S occurs.
Equations
- BSLambda.LLL.avoid Ev S = {ω : BSLambda.LLL.Cfg β | ∀ i ∈ S, ω ∉ Ev i}
Instances For
Membership in avoid.
Avoiding no events is the sure event.
Avoiding every event is avoiding all of them.
Avoiding more events is a smaller event.
Peeling one event off avoid.
avoid Ev S is determined by the union of the supports of the events indexed by S.
The local lemma #
The asymmetric Lovász local lemma (Section 10.2 of bs_lambda.txt). If each bad
event Ev i is determined by supp i and has probability at most
x i * ∏ j ∈ nbr supp i, (1 - x j) for some weights x i ∈ (0, 1), then with positive
probability no bad event occurs.
The two-type form #
The two-type asymmetric local lemma of Section 10.2 of bs_lambda.txt. Each event has a
type ty i : Bool, and events of type t have probability at most p t and at most D t s
neighbours of type s.
Pinning coordinates whose targets depend on other coordinates #
The event that a configuration agrees on G with the partial configuration c.
Equations
- BSLambda.LLL.fibre G c = {ω : BSLambda.LLL.Cfg β | ∀ (a : A) (ha : a ∈ G), ω a = c a ha}
Instances For
Every configuration lies in the fibre over its own restriction to G.
A fibre over G is determined by G.
Distinct partial configurations have disjoint fibres.
The fibres over G partition the configuration space, so their probabilities sum to 1.
Pinning with targets read off other coordinates. If, on the event E, every
coordinate of T lands in a target set of size at most m that depends only on the
coordinates of a set G disjoint from T, then E has probability at most
∏ a ∈ T, m / |β a|. This is the counting form of "condition on G; the coordinates of
T are still independent and uniform".
The constant-alphabet form of pr_le_prod_of_pinned, as used in Sections 8.1 and 9.