Email Gateway (Oct 16 2023 at 14:30): Email Gateway (Oct 16 2023 at 14:30):From: Tobias Nipkow <nipkow@in.tum.de>
Hypergraph Colouring Bounds
Chelsea Edmonds and Lawrence C. Paulson
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.
https://www.isa-afp.org/entries/Hypergraph_Colourings.html
Enjoy!
Last updated: Apr 29 2024 at 04:18 UTC