Hypergraph Colouring Bounds

This library includes several example applications of the probabilistic method for combinatorics to establish bounds for hypergraph colourings. This focuses on Property B - the existence of a two-colouring of the vertex set of a hypergraph. A stricter bound was formalised using the Lovász local lemma, which in turn required a surprisingly complex proof of the mutual independence principle for hypergraph edges that is often omitted on paper. The formalisation uncovered several interesting examples of circular intuition on proofs involving independence on paper. The formalisation is based on the textbook proofs from Alon and Spencer's famous textbook, The Probabilistic Method, further supported by notes by Zhao. The mutual independence principle proof is inspired by the less precise proof provided in Molloy and Reed's textbook on graph colourings, as it was omitted in all other sources. Additionally, this library demonstrates how locales can be used to establish a reusable probability space framework, thus minimizing the setup required for future formalisations requiring a probability space on numerous possible properties around an incidence system's vertex set.