(Unlabeled) enumerative combinatorics

Stream: mathlib4

[Mitchell Lee]

Hello, I was looking at some of the enumerative combinatorics in Mathlib; particularly Combinatorics/Catalan. In that file, treesOfNumNodesEq n is defined to be the set of all binary plane trees with n nodes, and it is proved that (treesOfNumNodesEq n).card equals $\frac{1}{n+1} \binom{2n}{n}$ using a recurrence relation. I believe that this proof benefits from being viewed from a different perspective, and that this different perspective will pay dividends in many future formalizations as well. The idea is that instead of doing the enumeration one value of $n$ at a time, we will do it for all values of $n$ at the same time.

Let $R$ be a complete filtered ring (usually a power series ring). A valued set (or class of valued combinatorial objects) is a pair $A = (A, v_A)$, where $A$ is a set and $v_A \colon A \to R$ is a function such that the sum

$$\sum_{a \in A} v_A(a)$$

converges. We define $|A| = |(A, v_A)| \in R$ to be the value of this sum. This is a slight generalization of a definition from Viennot's Introduction to Enumerative, Algebraic, and Bijective Combinatorics and a significant generalization of a definition from Flajolet's Analytic Combinatorics.

Examples.

• Any finite set $A$ may be viewed as a valued set by taking $v_A$ to be the function $a \mapsto 1$. In that case, $|A|$ is just the cardinality of the set $A$. In other words, anything that can be done with finite sets and cardinality can be done with valued sets as well.
• For any $t \in R$, the singleton ${\ast}$ can be given the valuation $\ast \mapsto t$. We will denote this valued set simply by the notation $t$. Then $|t| = t$.
• If $A$ and $B$ are valued sets, so is their disjoint union $A + B$. Of course, $|A + B| = |A| + |B|$. This can be extended to infinite sums as well, in certain cases.
• If $A$ and $B$ are valued sets, so is their Cartesian product $A \times B$, with valuation $v_{A \times B}(a, b) = v_{A}(a) v_{B}(b)$. Of course, $|A \times B| = |A| |B|$. This can be extended to infinite products as well, in certain cases.
• Given a valued set $A$ and a continuous ring homomorphism $\phi \colon R \to R'$ (actually, it can even be a continuous abelian group homomorphism), we may define the pushforward $\phi_*A$ to be the set $A$ equipped with the valuation $v_{\phi_*A} = \phi \circ v_A$. Then $|\phi_* A| = \phi(|A|)$.

Here is the valued form of the most important result in enumerative combinatorics:

(Obvious) Theorem.

If there is a bijection $f \colon A \to B$ that preserves valuations (i.e. $f \circ v_A = v_B$), then $|A| = |B|$.

(Almost) every general theorem about cardinality that's useful in enumerative combinatorics has an analogue for valued sets.

[Mitchell Lee]

To illustrate the usefulness of this concept, here are a few example applications.

Example applications

Binary plane trees

Let $R$ be the power series ring $\mathbb{Z}[\![t]\!]$. Let $\mathcal{C}$ be the set of all binary plane trees (of any size). In Lean, this would be represented by the type Tree True, or you could define it yourself using

inductive BinaryPlaneTree : Type
  | nil : BinaryPlaneTree α
  | node : BinaryPlaneTree α → BinaryPlaneTree α → BinaryPlaneTree α

For all $T \in \mathcal{C}$, define $v_{\mathcal{C}}(T)$ to be $t^n$, where $n$ is the number of nodes of $T$.

Then, there is an obvious valuation-preserving bijection between $\mathcal{C}$ and $1 + t \times \mathcal{C} \times \mathcal{C}$, so $|\mathcal{C}| = 1 + t|\mathcal{C}|^2$, whence

$$|\mathcal{C}| = \sum_{n} \frac{1}{n+1}\binom{2n}{n} t^n$$

by a routine computation using the Lagrange inversion theorem. Taking the coefficient of $t^n$ recovers the number of binary plane trees with $n$ nodes. That's it; no recurrence relations necessary.

Note: In order to formalize this, you must prove that there are finitely many binary plane trees with $n$ nodes, so you can conclude that $\mathcal{C}$ is actually a valued set. This might be the most difficult part of the proof.

Partitions

Again, let $R$ be the power series ring $\mathbb{Z}[\![t]\!]$, Let $\mathcal{P}$ be the set of all partitions, and for any partition $\lambda$ of size $n$, define $v_{\mathcal{P}}(\lambda) = t^{n}$.

For all $k \geq 1$, let $\mathcal{P}^{(k)}$ be the set of partitions that use only the part $k$. Then there is a valuation-preserving bijection between $\mathcal{P}$ and the convergent product $\prod_{k \geq 1} \mathcal{P}^{(k)}$, so

$$|\mathcal{P}| = \prod_{k \geq 1} |\mathcal{P}^{(k)}| = \prod_{k \geq 1} \frac{1}{1 - t^k}.$$

Using the "involution principle for valued sets", it is also possible to prove Euler's pentagonal number theorem. I will not go into the details.

Schur functions

Let $R$ be the ring of formal power series in infinitely many variables $x_1, x_2, x_3, \ldots$. For any partition $\lambda$, let $\operatorname{SSYT}(\lambda)$ be the set of semistandard Young tableaux of shape $\lambda$. Given an SSYT $T$, define $v(T) = x_1^{m_1(T)} x_2^{m_2(T)} x_3^{m_3(T)} \cdots$, where $m_i(T)$ is the number of times that $i$ appears in $T$. This turns $\operatorname{SSYT}(\lambda)$ into a valued set. Then the Schur function can be defined quite simply:

$$s_\lambda = |\operatorname{SSYT}(\lambda)|$$

To prove that this is a symmetric function in $x_1, x_2, x_3, \ldots$, it suffices to prove that it is fixed by any automorphism $\sigma \colon R \to R$ that permutes finitely many of the variables. This reduces to finding a valuation-preserving bijection between $\operatorname{SSYT}(\lambda)$ and the pushforward $\sigma_* \operatorname{SSYT}(\lambda)$, which can be done using the Bender-Knuth involutions.

So far, we haven't even used the cartesian product operation on valued sets that was so useful in our first two examples. But already, we have gained a lot from the concept of valued sets. Imagine all the steps that one would need to take in order to carry out the above argument using only finite sets and cardinality:

• For any finitely supported sequence $\mu = (\mu_1, \mu_2, \mu_3, \ldots)$, one would have to define the set $\operatorname{SSYT}(\lambda, \mu)$ of SSYT of shape $\lambda$ and content $\mu$, and prove that it is finite.
• Then, one would define $s_\lambda$ to be the formal power series whose coefficient of $x_1^{\mu_1} x_2^{\mu_2} x_3^{\mu_3} \cdots$ is the Kostka number $K_{\lambda, \mu} = \operatorname{SSYT}(\lambda, \mu)$.
• To prove that this is symmetric, one would need to find, separately for each sequence $\mu$ and each bijection $\sigma \colon \mathbb{N} \to \mathbb{N}$, a bijection between $\operatorname{SSYT}(\lambda, \mu)$ and $\operatorname{SSYT}(\lambda, \mu \circ \sigma)$.

The valued sets keep track of all the relevant information about $\mu$ automatically.

Using the Lindström–Gessel–Viennot lemma, one may then prove the Jacobi-Trudi identity

$$s_\lambda = \det (h_{\lambda + j - i})_{i, j = 1}^\ell$$

directly. Normally, this would require truncating the power series $s_\lambda$ at a finite number of variables so that the sums involved are finite, applying the Lindström–Gessel–Viennot lemma to a finite graph, and then taking a limit. But if everything is done using valued sets, this is not necessary.

[Mitchell Lee]

Questions

• Does the concept of a "valued set" belong in Mathlib?
• If so, what should be the exact definition? Is "complete filtered ring" the correct level of generality for $R$? Should $R$ be restricted to be a power series ring? Should it be allowed to be something even more general?
• If we decide that $R$ is only allowed to be a power series ring, then should the values of the function $v_A$ only be allowed to be monomials?

Once these questions are answered, I would be happy to start working on formalizing some of the things in this message.

[Mitchell Lee]

I realize now I probably made this post too long to expect anyone to read. Here is the short summary:

• Rather than considering only "unweighted" finite sets and their cardinalities, it is often useful in enumerative combinatorics to consider the more general "weighted" notion of a valued set, which is a (possibly infinite) set together with a summable valuation function $v_A \colon A \to R$, where $R$ is a power series ring (or more generally, a complete ring with a descending filtration of ideals). Each valued set $A$ has a value $|A| \in R$, analogous to the cardinality of a finite set. If $v_A$ is the constant function $1$, we recover the usual notion of cardinality.
• The familiar notions of disjoint union and cartesian product can be performed for valued sets, with the familiar equations $|A + B| = |A| + |B|$ and $|A \times B| = |A| \times |B|$.
• The bijection principle also holds, if the bijection preserves the valuation.
• Combinatorialists use this concept all the time, even if they don't say they are using it.
• I would like this (or a concept like it) to be in Mathlib, but I want to make sure that I have defined everything in the most usable possible way first.

[Scott Carnahan]

I am relatively new to mathlib, but I think a powerful tool that could be applied to multiple existing results would be welcome.
When you say that the sum converges (in the defining condition, second paragraph of the top post), do you mean some kind of finite co-support condition, i.e., for any filtration degree d, there are only finitely many terms outside the d-th filtered part?

[Mitchell Lee]

Yes, that's what I mean.

[Ruben Van de Velde]

Calling our resident combinatorist, @Yaël Dillies

[Yaël Dillies]

(I read the messages but haven't formulated a response yet :smile:)

[Mitchell Lee]

I just want to make sure that I don't end up setting things up in a way that is annoying or frustrating to use. I don't want to actually think about filtered rings and continuity while doing combinatorics, but I think that if everything is done properly, all that stuff can just be "under the hood", as it were.

[Yaël Dillies]

I just opened #11666 to create a Combinatorics.Enumerative folder.

[Mitchell Lee]

Thank you.

I realized today that there is no need to reinvent the wheel. The concept of unconditional summability is already in Mathlib: docs#Summable. A valued set is really the same thing as an unconditionally summable function v : A → R, where R is a topological abelian group. It does not need its own definition.

Nor do we really need R to be a complete ring with a descending filtration of ideals; it just needs to be a nonarchimedean ring (docs#NonarchimedeanRing).

With this perspective, the disjoint union of valued sets doesn't need its own definition either; it is just docs#Sum.elim (or, for arbitrary sums, docs#Sigma.uncurry). It should even be pretty easy to prove the relevant theorems. Pushforward is similarly easy to define; it's just docs#Function.comp.

Only two things would actually be needed in order to carry out the Catalan number argument I mentioned in my first post. First, a theorem like this for taking the product of two sums in a nonarchimedean ring:

theorem Summable.mul_of_nonarchimedean {ι ι' R : Type*} [Ring R] [TopologicalSpace R] [NonarchimedeanRing R]
    {f : ι → R} {g : ι' → R} (hf : Summable f) (hg : Summable g) :
    Summable fun (x : ι × ι') ↦ f x.1 * g x.2 := by
  sorry

And second, an actual NonarchimedeanRing instance on the power series ring.

[Daniel Geisler]

Hello @Mitchell Lee , I'm new to Lean and just joined this Zulip community. I'll be rereading and sharing your posting.

My research is in extending tetration and fractional iteration. I start with Faà di Bruno's formula as the connection between the derivatives of composite functions, integer partitions and set partitions. These can be generalized to the derivatives of iterated functions, unlabeled total partitions and total partitions. My first step is to write a proof for Faà di Bruno's formula.

[Mitchell Lee]

I just opened #11688, which proves that a sum in a complete nonarchimedean abelian group is unconditionally summable if and only if the terms tend to zero on the cofinite filter. I will work on the mul_of_nonarchimedean lemma next.

[Ralf Stephan]

Coming to this thread because of interest in formalizing enumerative combinatorics basic results. I'm looking at the introduction of Miklos Bona's Handbook, and I'm asking myself if my domino tiling definition attempt at
https://github.com/rwst/lean-code/blob/main/domino.lean
is the right way to do it. What do you think?

Also @Mitchell Lee , isn't the series you're proposing but one aspect of the generating function (which has other useful aspects)? Given this, how to introduce the g.f. concept?

[Yaël Dillies]

I think your definition is cumbersome. You should probably take a completely different approach by looking at docs#MeasureTheory.IsFundamentalDomain

[Mitchell Lee]

I agree with taking a completely different approach. A domino tiling of a rectangle can be described as a perfect matching of a grid graph. These concepts are already in mathlib. This formulation is sufficient to state most important results about domino tilings (Kasteleyn's formula, the arctic circle theorem, etc.).

[Yaël Dillies]

Here is the general definition of (discrete) tilings I would use:

import Mathlib.Data.Finset.Pointwise
import Mathlib.Order.Partition.Finpartition

open scoped Pointwise

variable (G : Type*) {α : Type*} [AddGroup G] [AddAction G α] [DecidableEq α]

/-- A `G`-tiling of a finset `s` by `shapes` is a finite partition of `s` by finsets such that
every part is a translate of some shape in `shapes`. -/
structure DiscreteTiling (shapes : Set (Finset α)) (s : Finset α) extends Finpartition s where
  exists_translate_of_mem_parts' {part} :
    part ∈ toFinpartition.parts → ∃ g : G, ∃ shape ∈ shapes, g +ᵥ shape = part

[Yaël Dillies]

Eg domino tilings would be DiscreteTiling (ℤ × ℤ) ({{(0, 0), (0, 1)}, {(0, 0), (1, 0)}} : Set (Finset (ℤ × ℤ))) (Finset.Icc 0 n)

[Yaël Dillies]

For dominoes, I agree that the perfect matching approach is easier to work with, but for general discrete tilings I quite like the above

[Joseph Myers]

I have a somewhat more complicated definition of discrete tilings (oriented to reasoning about tilings of infinite spaces with infinitely many tiles, though it can certainly be applied in a finite context) in AperiodicMonotilesLean (not yet PRed to mathlib because I'd like to formalize some results with actual mathematical content before PRing new definitions, and I was never expecting to have time for much work on this project from April through July). The definitions I'm using allow for asymmetrically marked tiles (so two copies of a tile that have the same points can still be considered different), and the basic tiling-like type used is for indexed families of tiles, with the property of being a tiling just being one function on indexed families of tiles and most lemmas working with weaker properties. (Functions on indexed families of tiles, and properties of such functions, seem to be something that comes up naturally when trying to express formal statements in appropriate generality - not something so much in the informal literature where people don't try so much for that generality.)