Combinatorics

Stream: general

[Yaël Dillies]

For your information, I'm now trying to get #2770 in mathlib. This (old!) monster PR from Bhavik Mehta includes:

• the Lubell-Yamamoto-Meshalkin inequality
• Sperner's theorem
• the Kruskal-Katona theorem
• the Erdős-Ko-Rado theorem

in case anybody happens to be working on this.

[Bhavik Mehta]

I know @Ryan Lahfa and @Alena Gusakov both tried to update this but moved on to other things, as did I - although stuff like the colex ordering did come out of that. I mostly made that PR so that it wouldn't get forgotten and so that if people search mathlib for those results they appear

[Yaël Dillies]

Antichains are also now part of mathlib! docs#is_antichain
Next thing on my TODO list is shadow

[Yaël Dillies]

Both #10223 (shadow) and #10238 (UV compression) are up for review!

[Yaël Dillies]

Shadows are now in mathlib and UV compressions (#10238, +242, -0) are still up for review.
I'm now hitting a few very easy but very useful definitions:

/-- `all_sized A r` states that every set in A has size r. -/
def all_sized (A : finset (finset α)) (r : ℕ) : Prop := ∀ x ∈ A, card x = r

/-- The `r`th slice of a set family the subset of its elements which have cardinality `r`. -/
def slice (𝒜 : finset (finset α)) (r : ℕ) : finset (finset α) := 𝒜.filter (λ i, i.card = r)

What do you prefer between putting them under data.finset. and combinatorics.set_family?

[Eric Wieser]

How does the alternative strategy of defining a type for finsets of card n (as vector is to list) go?

[Yaël Dillies]

and sym is to multiset

[Yaël Dillies]

For unrelated reasons I actually wanted to do that, so I'll consider the option! In the context of set families, it's probably a bit weird, because your goal is to stratify the membership hypercube, not to look at a single layer.

[Bhavik Mehta]

Eric Wieser said:

How does the alternative strategy of defining a type for finsets of card n (as vector is to list) go?

I tried this in a super early version of these results, about 2 years ago, and on the advice of someone here I changed to the current versions for the purposes of Kruskal-Katona, and it made that go a lot more smoothly. But this doesn't mean that defining that type for other purposes could still be useful, it's just that in this case it made things a lot worse

[Yaël Dillies]

#13149 (+207, -13) proves that UV-compression reduces the size of the shadow. This is mostly one big monstruous proof, so it is up for golfing!