General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma (Q7361462)

This entry aims to formalise several useful general techniques for using the probabilistic method for combinatorial structures (or discrete spaces more generally). In particular, it focuses on bounding tools for combinatorics, such as the union and complete independence bounds, and the first formalisation of the pivotal Lov&aacutesz local lemma. The formalisation focuses on the general lemma, however also proves several useful variations, including the more well-known symmetric version. Both the original formalisation and several of the variations used dependency graphs, which were formalised using Noschinski's general directed graph library. Additionally, the entry provides several useful existence lemmas, required at the end of most probabilistic proofs on combinatorial structures. Finally, the entry includes several significant extensions to the existing probability libraries, particularly for conditional probability (such as Bayes theorem) and independent events. The formalisation is primarily based on Alon and Spencer's textbook "The Probabilistic Method", as well as Zhao's course notes on the subject.