balanced partitions

Stream: graph theory

[Mauricio Collares]

I have half-Lean half-pseudocode file with a sketch of Turán-related things (Turán graphs, Turán numbers and Turán's theorem) and I am slowly converting it into actual Lean code. One of the very first things is to define a balanced k-partition of an n-vertex graph, which means that the parts have size as equal as possible. Lean is happy if I add the code below to simple_graph/partition.lean (after the variables {G} (P : G.partition) line)...

open_locale classical

def partition.is_balanced [fintype V] : Prop :=
∀ (p₁ p₂ ∈ P.parts), |(fintype.card p₁ - fintype.card p₂ : ℤ)| ≤ 1

...but I don't know how to add the typeclasses needed to replace open_locale classical, and I also don't want to add open_locale classical to a preexisting file. What should I do?

Also: I looked at docs#order.partition.finpartition in an attempt, but the latter insists on the empty set not being a part, which would be problematic in my application ((n,k)-Turán graphs with n < k are still Turán graphs). I guess this means SzRL requires a "n sufficiently large" assumption? There are many slight variations in the statement of SzRL, but I am used to is "For every $m \in \mathbb{N}$ and $\varepsilon > 0$, there exists $M \in \mathbb{N}$ such that every graph admits an $\varepsilon$-regular partition with k parts, where $m \leq k \leq M$", which I find quite elegant.

[Mauricio Collares]

Huh, not only my code snippet no longer compiles (emacs must have died on me before, because it was not complaining), I just nocited docs#simple_graph.partition also forbids empty sets in the partition. This is very surprising for combinatorics; I have never seen a book saying "G is bipartite if its vertex set can be partitioned into at most two non-empty independent sets".

[Kyle Miller]

The combinatorics textbook I used for my course this quarter said that a bipartite graph had two nonempty parts for its partition, for what it's worth.

One of the reasons for forbidding empty sets is the bad behavior when you talk about, say, a tripartite graph. If you allow the empty set, then you're only allowed up to one empty set.

[Kyle Miller]

finpartition requires that there be only finitely many parts, which is why simple_graph.partition doesn't use it. The graph coloring part of the library goes back and forth between colorings and graph partitions, and it supports infinite color sets.

[Mauricio Collares]

Kyle Miller said:

The combinatorics textbook I used for my course this quarter said that a bipartite graph had two nonempty parts for its partition, for what it's worth.

One of the reasons for forbidding empty sets is the bad behavior when you talk about, say, a tripartite graph. If you allow the empty set, then you're only allowed up to one empty set.

At most two nonempty parts, I assume? That definition is equivalent but (subjectively) it has a very "uncanny valley" quality to it. This kind of mismatch is common even inside combinatorics (e.g., $P_k$ has k edges for me, but k vertices for some people), but I must say I still find this one a bit surprising.

[Mauricio Collares]

I see what you mean about empty sets, but I would expect a $k$-partition to be a $k$-tuple of pairwise disjoint independent sets whose union is $V$, because even in the bipartite case you typically want to refer to "the left part" and "the right part".

[Mauricio Collares]

What I said is not really true, I guess. Most places I know define it with a variation of "A k-partite graph is one whose vertex set can be partitioned into k subsets, or parts, in such a way that no edge has both ends in the same part", sidestepping the issue of representing it with a tuple/multiset. This particular quote is from Bondy and Murty, but it captures well what I think of as the "common" definition.

[Mauricio Collares]

(deleted)

[Yaël Dillies]

You probably want to use docs#set.is_equitable anyway.

[Yaël Dillies]

Kyle Miller said:

finpartition requires that there be only finitely many parts, which is why simple_graph.partition doesn't use it.

There are four flavors of partitions:

• partitions (docs#setoid.is_partition)
• finite partitions (docs#finpartition)
• partitions in finite sets (docs#simple_graph.partition)
• finite partitions in finite sets

[Mauricio Collares]

I am happy with using equitable, thanks! Even in "paper math" I find it funny that people call them "balanced partitions" and "equitable colorings".

[Kyle Miller]

Mauricio Collares said:

At most two nonempty parts, I assume?

The problem is that it's a set (set V), so it can only have at most one part that is the empty set, since any two empty sets are equal. Requiring that all the parts be nonempty seemed to be the best way to avoid this set theory technicality.

If you want to identify which partition is what, then what you can do is instead work with graph colorings. In that context, parts (i.e., color sets) are allowed to be empty.

[Kyle Miller]

This application is sort of an intended use of graph colorings.

[Mauricio Collares]

I see your point, but I'm just saying that this would be surprising to every combinatorialist I know. I mean, most of them wouldn't care in general, but I estimate everyone I know would say "Yes" when asked if a $2$-vertex graph is $4$-partite.

[Kyle Miller]

Yaël Dillies said:

There are four flavors of partitions:

• partitions (docs#setoid.is_partition)
  ...

• partitions in finite sets (docs#simple_graph.partition)
  ...

Did you mean to link to something other than docs#simple_graph.partition? Those are plain partitions using docs#setoid.is_partition

[Kyle Miller]

@Mauricio Collares I agree, though the docstrings at docs#simple_graph.partition.parts_card_le and docs#simple_graph.partitionable at least try to explain what n-partite means in the context of the mathlib

[Kyle Miller]

It could be better documented, especially since it doesn't mention that it it's n-partite in the unlabeled sense.

[Kyle Miller]

This is probably one of those examples where formalization is made difficult by the informal way combinatorics is handled. It can be hard to pin down what a combinatorialist means by a partition, and we have simple_graph.partition and simple_graph.coloring with somewhat different properties. The module docstring on the partitions module describes the relationship between the two.

[Mauricio Collares]

Agreed. It just feels bittersweet to have to translate terms between "actual math" and "formalized math" so early in the process :) But I guess this is a common feeling with computer maths, I just haven't gotten used to it yet.

[Kyle Miller]

De Bruijn commented about this in an AMS Notices article as hitting combinatorics particularly hard, since more abstract math tends to be formalized to some degree already

[Mauricio Collares]

I mean, I don't expect actual theorems to have any such difficulty, only definitions. And it's certainly the case that different subareas of combinatorics tend to optimize notation for their particular problems, so people are somewhat used to the different definitions.

[Kyle Miller]

(Here's his article: https://pure.tue.nl/ws/files/4388246/599163.pdf)

[Mauricio Collares]

For example, I work on extremal combinatorics, where "contains a copy of $H$" does not mean "induced". I am used to mentally translating such terms when talking to friends who work in structural combinatorics.

[Mauricio Collares]

(But I honestly think we have consensus on not disallowing empty sets/multiple empty sets when defining $k$-partitions and $k$-partite graphs, which is why I am dwelling on it so much.)

[Kyle Miller]

Yeah, we do have that consensus, it's just not reflected in the partition type due to the set theory technicality. You're meant to use either a partition satisfying P.parts_card_le k or a fin k graph coloring for a k-partite graph

[Kyle Miller]

Another version of the graph partition type could include a natural number counting the number of empty parts, but a problem with that is that it doesn't allow more than finitely many empty parts...

[Mauricio Collares]

I really appreciate the time you're taking to reply! I will just keep going with one of these alternatives. Naïvely my mind goes to "why not just use multiset (set V)", but I guess we wouldn't be able to reuse the "standard" set partition API, which I can see being troublesome.

[Mauricio Collares]

Ah, wait, are multisets always finite in mathlib?

[Kyle Miller]

Yeah, they are

[Mauricio Collares]

Ah, that's the piece of information I didn't have before! I see now.

[Mauricio Collares]

Thanks for the explanation!

[Kyle Miller]

But it's still an interesting idea for allowing multiple copies of the empty set.

[Mauricio Collares]

I wonder how many people use graph partitions with an infinite number of parts. Although I like to take $n$ to infinity a lot, I don't work in infinite combinatorics. If they always use colorings instead of partitions, that would solve the issue.

[Mauricio Collares]

In hindsight, I think I was just being stupid/stubborn. It's probably OK to define a $(n,k)$-Turán graph as something that is either a complete graph if $n < k$ or a $k$-partite complete balanced graph if $n \geq k$.

[Mauricio Collares]

Or I could define a partition as $k$-equitable if it either is equitable with $k$ parts or it has fewer than $k$ parts and all parts are singletons (i.e., its "zero-padded" version is equitable).