# Zulip Chat Archive

## Stream: graph theory

### Topic: balanced partitions

#### Mauricio Collares (Jun 23 2022 at 11:07):

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 (Jun 23 2022 at 16:12):

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 (Jun 23 2022 at 16:15):

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 (Jun 23 2022 at 16:18):

`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 (Jun 23 2022 at 16:21):

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 (Jun 23 2022 at 16:22):

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 (Jun 23 2022 at 16:29):

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 (Jun 23 2022 at 16:31):

(deleted)

#### Yaël Dillies (Jun 23 2022 at 16:37):

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

#### Yaël Dillies (Jun 23 2022 at 16:38):

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 (Jun 23 2022 at 16:39):

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 (Jun 23 2022 at 16:42):

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 (Jun 23 2022 at 16:44):

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

#### Mauricio Collares (Jun 23 2022 at 16:46):

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 (Jun 23 2022 at 16:46):

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 (Jun 23 2022 at 16:48):

@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 (Jun 23 2022 at 16:48):

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

#### Kyle Miller (Jun 23 2022 at 16:51):

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 (Jun 23 2022 at 16:52):

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 (Jun 23 2022 at 16:54):

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 (Jun 23 2022 at 16:55):

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 (Jun 23 2022 at 16:56):

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

#### Mauricio Collares (Jun 23 2022 at 16:57):

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 (Jun 23 2022 at 16:59):

(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 (Jun 23 2022 at 17:02):

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 (Jun 23 2022 at 17:03):

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 (Jun 23 2022 at 17:06):

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 (Jun 23 2022 at 17:07):

Ah, wait, are multisets always finite in mathlib?

#### Kyle Miller (Jun 23 2022 at 17:07):

Yeah, they are

#### Mauricio Collares (Jun 23 2022 at 17:08):

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

#### Mauricio Collares (Jun 23 2022 at 17:08):

Thanks for the explanation!

#### Kyle Miller (Jun 23 2022 at 17:08):

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

#### Mauricio Collares (Jun 23 2022 at 17:15):

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 (Jun 23 2022 at 17:35):

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 (Jun 23 2022 at 17:38):

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).

Last updated: Dec 20 2023 at 11:08 UTC