Email Gateway (Sep 22 2023 at 11:07): Email Gateway (Sep 22 2023 at 11:07):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
there are two further AFP entries from the Cambridge team, this time by Chelsea.
Hypergraphs
by Chelsea Edmonds
This entry is a simple extension of the Combinatorial design theory library,
which presents new and existing concepts using hypergraph language. Both designs
and hypergraphs are types of incidence set systems and hence have the same
underlying foundation. However, they are often used in different contexts, and
some definitions are unique. This library uses locales to rewrite equivalent
definitions and build a basic hypergraph hierarchy with direct links to
equivalent design theory concepts to avoid repetition, further demonstrating the
power of the "locale-centric" approach. The library includes all standard
definitions (order, degree etc.), as well as some extensions on hypergraph
decompositions and spanning subhypergraphs.
https://www.isa-afp.org/entries/Hypergraph_Basics.html
General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma
by Chelsea Edmonds
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ász 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.
https://www.isa-afp.org/entries/Lovasz_Local.html
Enjoy,
René
Last updated: Apr 28 2024 at 20:16 UTC