A finite product probability space #
The probabilistic input to the Lovász local lemma of Section 10 of bs_lambda.txt is a
uniformly random assignment of a label to each of finitely many independent coordinates.
We model this by plain counting over the finite product type Cfg β = ∀ a, β a; no measure
theory is involved.
An event E : Finset (Cfg β) is determined by a coordinate set S when membership in E
only depends on the restriction of a configuration to S. Two events determined by disjoint
coordinate sets are independent (pr_inter_of_disjoint_support); this is the only
probabilistic input the local lemma needs.
pr E is E.dens, the density of E in the space of all configurations, viewed as a real
number; pr_eq_div is the corresponding quotient of cardinalities.
Besides independence the file provides finite additivity (pr_biUnion), the union bound
(pr_biUnion_le) and the counting probabilities of the pinning events "coordinate a lands
in s a for every a ∈ T" (pr_coord_mem, pr_pin_eq, pr_pin_le).
Adapted for Lean Pool from Timeroot/BS_Lam at commit
7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.
A configuration: an assignment of a value to every coordinate.
Equations
- BSLambda.LLL.Cfg β = ((a : A) → β a)
Instances For
The uniform counting probability of an event: its density in the space of all configurations.
Equations
- BSLambda.LLL.pr E = ↑E.dens
Instances For
The empty event has probability zero.
The number of configurations is positive, so the counting probability is well defined.
The whole space has probability one.
Finite additivity. The probability of a union of pairwise disjoint events is the sum of the probabilities.
The complementary form of pr_inter_add_pr_compl_inter.
The union bound. The probability of a finite union is at most the sum of the probabilities.
The union bound in the form used to cover an event by an enumeration of cases.
An event determined by S is determined by any larger coordinate set.
The intersection of two determined events is determined by the union of the supports.
The complement of a determined event is determined by the same coordinates.
The standard way to exhibit a determined event: an event cut out of the whole space by a
predicate that only reads the coordinates in S.
The event that one coordinate lands in a prescribed set is determined by that coordinate.
A pinning event is determined by the coordinates it pins.
An event determined by a set disjoint from S only sees the off-S half of a glued
configuration.
The involution (u, v) ↦ (glue S u v, glue S v u) used to prove independence.
Equations
- BSLambda.LLL.swapGlue S p = (BSLambda.LLL.glue S p.1 p.2, BSLambda.LLL.glue S p.2 p.1)
Instances For
Independence. Two events determined by disjoint sets of coordinates are independent
for the uniform counting probability. This is the probabilistic input to the local lemma of
Section 10 of bs_lambda.txt.
Counting core. Pinning one coordinate to a prescribed value divides the number of configurations by the size of that coordinate's alphabet.
A single coordinate takes a prescribed value with probability 1 / |β a|.
A single coordinate lands in a prescribed set with probability |s| / |β a|.
Pinning several coordinates. Distinct coordinates are independent, so the probability that each of them lands in a prescribed set is the product of the individual probabilities.
Pinning several coordinates into target sets of size at most m.