Extremal graph theory

Stream: graph theory

[John Talbot]

Hello! I'm interested in helping add results from extremal graph theory to mathlib.

@Yaël Dillies I know you're working on Turan's theorem (via Furedi's stability result) which is fantastic and I'd be very happy to help!

Together with a student we have formalized the Andrasfai-Erdos-Sos theorem (following Brandt's proof).

theorem aes_brandt (hf: G.CliqueFree (r + 2)) (hd : (3 * r - 1) * (Fintype.card α) / (3 * r + 2) < G.minDegree) :
    G.Colorable (r + 1)

It would be nice to get this into mathlib at some point but I was hoping to start with something smaller.

For example we have:

theorem chromaticNumber_eq_card_of_forall_surj [Fintype α] (C : G.Coloring α)
    (h : ∀ C' : G.Coloring α, Function.Surjective C') : G.chromaticNumber = Fintype.card α

but not (as far as I can see)

theorem chromaticNumber_eq_card_iff_forall_surj [Fintype α] (C : G.Coloring α) :
    G.chromaticNumber = Fintype.card α  ↔ (∀ C': G.Coloring  α, Function.Surjective C')

Would this be a useful addition?

Suggestions of where to start would be very welcome!

[Kevin Buzzard]

Simple and useful results which build up the API for a concept already in mathlib are essentially always welcome, and will be a great introduction to the PR process (which is more nontrivial than people sometimes realise). Please feel free to open a short PR!

[John Talbot]

Thanks for the tips, I'll start as small as possible!

[Kyle Miller]

chromaticNumber_eq_card_iff_forall_surj looks like a good addition, please open a PR!