Noncrossing partitions and noncrossing pairings are counted by the Catalan numbers

Let s be a nonempty finite set of positions in a linear order, with first position m. For a noncrossing partition P of s, let x be the last position of the part of P containing m. No part of P then joins a position before x to a position after x, so P is the same as a noncrossing partition of the positions of s before x (with x adjoined to the part of m) together with an arbitrary noncrossing partition of the positions of s after x. This is the recurrence of noncrossing partitions by the part containing the first position, and it is the recurrence of the Catalan numbers; hence there are catalan n noncrossing partitions of n ordered positions. In this decomposition the parts of P other than the part of m are those of the two pieces, so the recurrence also holds for sums of products of weights of the parts, with the part of m weighted separately; this is the form used to compute weighted sums over noncrossing partitions by generating functions.

The same decomposition counts the noncrossing pairings, the noncrossing partitions all of whose parts have two elements, which index the moments of semicircular variables. In a noncrossing pairing of s the first position m is paired with some x > m, and the pairing is the same as a noncrossing pairing of the positions strictly between m and x together with one of the positions after x. Hence there are catalan n noncrossing pairings of 2 * n ordered positions, and none of an odd number of positions.

Main results

• TauCeti.NoncrossingPartition.sum_mul_prod_eq_sum_mul_sum — the weighted recurrence by the part containing the first position m: with the part of m weighted by G and the other parts by F, the sum over NC(s) is the sum over x ∈ s of the sum over NC(s_{<x}), with x adjoined to the part of m, times ∑_{R ∈ NC(s_{>x})} ∏_{B ∈ R} F B.
• TauCeti.NoncrossingPartition.card_eq_sum_card_mul_card — the recurrence by the part containing the first position: |NC(s)| = ∑_{x ∈ s} |NC(s_{<x})| |NC(s_{>x})|.
• TauCeti.NoncrossingPartition.card_eq_catalan — |NC(s)| = catalan |s|.
• TauCeti.NoncrossingPartition.card_fin_eq_catalan — |NC(n)| = catalan n for the positions of Fin n.
• TauCeti.NoncrossingPartition.card_isPairing_eq_sum — the recurrence of noncrossing pairings by the partner x of the first position m: |NC₂(s)| = ∑_{x ∈ s, m < x} |NC₂(s ∩ (m, x))| |NC₂(s_{>x})|.
• TauCeti.NoncrossingPartition.card_isPairing_eq_catalan — |NC₂(s)| = catalan n when |s| = 2 n, and card_isPairing_eq_zero — |NC₂(s)| = 0 when |s| is odd.
• TauCeti.NoncrossingPartition.card_isPairing_fin_eq_catalan — |NC₂(2n)| = catalan n for the positions of Fin (2 * n).
• TauCeti.NoncrossingPartition.sum_prod_ite_card_eq_two — weighting the parts of size two by v and all others by 0, the noncrossing partitions of 2 n positions have total weight v ^ n * catalan n, and those of an odd number of positions total weight 0.

References

• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, Lecture 9.
• G. Kreweras, Sur les partitions non croisées d'un cycle, Discrete Math. 1 (1972), 333–350.

theorem TauCeti.NoncrossingPartition.sum_mul_prod_eq_sum_mul_sum {α : Type u_1} [LinearOrder α] {s : Finset α} {M : Type u_2} [CommSemiring M] (hs : s.Nonempty) (G F : Finset α → M) : ∑ P : NoncrossingPartition s, G ((↑P).part (s.min' hs)) * ∏ B ∈ (↑P).parts with s.min' hs ∉ B, F B = ∑ x ∈ s, (∑ L : NoncrossingPartition ({y ∈ s | y < x}), G (insert x ((↑L).part (s.min' hs))) * ∏ B ∈ (↑L).parts with s.min' hs ∉ B, F B) * ∑ R : NoncrossingPartition ({y ∈ s | x < y}), ∏ B ∈ (↑R).parts, F B

The weighted recurrence of noncrossing partitions by the part containing the first position m, with the part of m weighted by G and every other part weighted by F: the noncrossing partitions of s in which the part of m ends at x are the pairs of a noncrossing partition L of the positions before x, in which the part of m is extended by x, and a noncrossing partition of the positions after x.

theorem TauCeti.NoncrossingPartition.card_eq_sum_card_mul_card {α : Type u_1} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : Fintype.card (NoncrossingPartition s) = ∑ x ∈ s, Fintype.card (NoncrossingPartition ({y ∈ s | y < x})) * Fintype.card (NoncrossingPartition ({y ∈ s | x < y}))

The recurrence of noncrossing partitions by the part containing the first position: the noncrossing partitions of s in which that part ends at x correspond to the pairs of a noncrossing partition of the positions before x and one of the positions after x.

theorem TauCeti.NoncrossingPartition.card_eq_catalan {α : Type u_1} [LinearOrder α] (s : Finset α) : Fintype.card (NoncrossingPartition s) = catalan s.card

The noncrossing partitions of a finite set s of positions in a linear order are counted by the Catalan number catalan #s.

theorem TauCeti.NoncrossingPartition.card_fin_eq_catalan (n : ℕ) : Fintype.card (NoncrossingPartition Finset.univ) = catalan n

There are catalan n noncrossing partitions of the n ordered positions of Fin n.

theorem TauCeti.NoncrossingPartition.card_isPairing_eq_sum {α : Type u_1} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) : Fintype.card { P : NoncrossingPartition s // (↑P).IsPairing } = ∑ x ∈ s with s.min' hs < x, Fintype.card { M : NoncrossingPartition ({y ∈ s | s.min' hs < y ∧ y < x}) // (↑M).IsPairing } * Fintype.card { R : NoncrossingPartition ({y ∈ s | x < y}) // (↑R).IsPairing }

The recurrence of noncrossing pairings by the partner of the first position m: the noncrossing pairings of s in which m is paired with x correspond to the pairs of a noncrossing pairing of the positions strictly between m and x and one of the positions after x.

theorem TauCeti.NoncrossingPartition.card_isPairing_eq_zero {α : Type u_1} [LinearOrder α] {s : Finset α} (hs : Odd s.card) : Fintype.card { P : NoncrossingPartition s // (↑P).IsPairing } = 0

A finite set of odd size has no noncrossing pairing.

theorem TauCeti.NoncrossingPartition.card_isPairing_eq_catalan {α : Type u_1} [LinearOrder α] {s : Finset α} {n : ℕ} (hn : s.card = 2 * n) : Fintype.card { P : NoncrossingPartition s // (↑P).IsPairing } = catalan n

The noncrossing pairings of a finite set of 2 * n positions in a linear order are counted by the Catalan number catalan n.

theorem TauCeti.NoncrossingPartition.card_isPairing_fin_eq_catalan (n : ℕ) : Fintype.card { P : NoncrossingPartition Finset.univ // (↑P).IsPairing } = catalan n

There are catalan n noncrossing pairings of the 2 * n ordered positions of Fin (2 * n).

theorem TauCeti.NoncrossingPartition.sum_prod_ite_card_eq_two {α : Type u_1} [LinearOrder α] {M : Type u_2} [CommSemiring M] (s : Finset α) (v : M) : (∑ P : NoncrossingPartition s, ∏ B ∈ (↑P).parts, if B.card = 2 then v else 0) = if Even s.card then v ^ (s.card / 2) * ↑(catalan (s.card / 2)) else 0

Weighting each part of size two by v and every other part by 0, the total weight of the noncrossing partitions of s is v ^ (#s / 2) * catalan (#s / 2) for #s even and 0 for #s odd: only the noncrossing pairings contribute, each with weight v ^ (#s / 2). These are the moments of a semicircular element of variance v, whose only nonzero free cumulant is the second one.