Notations and Elementary Facts + Examples

This file formalizes the introductory material from the first chapter of the Algebraic Combinatorics course notes. It covers:

1. Basic combinatorial principles (addition, multiplication, bijection)
2. Binomial coefficient definitions and properties
3. Four motivating examples using generating functions:
   • The Fibonacci sequence and Binet's formula
   • Dyck words and Catalan numbers
   • The Vandermonde convolution identity
   • Solving a linear recurrence

Main Definitions

• FPS.fibonacci - The Fibonacci sequence (equivalent to Nat.fib in Mathlib)
• FPS.catalan - The Catalan numbers (equivalent to catalan in Mathlib)
• FPS.isDyckWord - Predicate for Dyck words (alternative to Mathlib's DyckWord structure)
• FPS.goldenRatioPlus - The golden ratio (equivalent to Real.goldenRatio in Mathlib)
• FPS.goldenRatioMinus - The conjugate golden ratio (equivalent to Real.goldenConj in Mathlib)

Main Results

• FPS.binom_def_formula - Definition \ref{def.binom.binom}: $\binom{r}{n} = \frac{r(r-1)\cdots(r-n+1)}{n!}$
• FPS.binom_factorial_smul - The factorial formula: $n! \cdot \binom{r}{n} = r(r-1)\cdots(r-n+1)$
• FPS.binom_natCast - For natural numbers: $\binom{n}{k} = $ Nat.choose n k
• FPS.binom_zero_right - Base case: $\binom{r}{0} = 1$
• FPS.binom_zero_left_pos - For $k > 0$: $\binom{0}{k} = 0$
• FPS.binom_one_right - First case: $\binom{r}{1} = r$
• FPS.binom_neg_one - The binomial coefficient $\binom{-1}{k} = (-1)^k$
• FPS.binom_two_n_n_eq - Formula $\binom{2n}{n} = \frac{1 \cdot 3 \cdot 5 \cdots (2n-1)}{n!} \cdot 2^n$
• FPS.pascal_identity - Pascal's identity for binomial coefficients (natural numbers)
• FPS.pascal_identity_ring - Pascal's identity for generalized binomial coefficients (binomial rings)
• FPS.pascal_identity_succ - Pascal's identity in successor form
• FPS.pascal_identity_int - Pascal's identity for integers
• FPS.pascal_identity_rat - Pascal's identity for rationals
• FPS.binom_zero_of_lt - $\binom{m}{n} = 0$ when $m < n$ for natural numbers
• FPS.binom_symm - Symmetry: $\binom{n}{k} = \binom{n}{n-k}$ (Theorem \ref{thm.binom.sym})
• FPS.binom_symm_add - Symmetry variant: $\binom{a+b}{a} = \binom{a+b}{b}$
• FPS.binom_symm_of_eq_add - Symmetry when $n = a + b$
• FPS.binom_symm_ring - Symmetry for Ring.choose (generalized binomial coefficients)
• FPS.fibonacci_binet - Binet's formula for Fibonacci numbers
• FPS.fibonacci_gf - Generating function $F(x) = x/(1-x-x^2)$
• FPS.catalan_recurrence - Recurrence $c_n = \sum_{k=0}^{n-1} c_k c_{n-1-k}$
• FPS.catalan_explicit - Explicit formula $c_n = \frac{1}{n+1}\binom{2n}{n}$
• FPS.vandermonde_convolution - $\binom{a+b}{n} = \sum_{k=0}^n \binom{a}{k}\binom{b}{n-k}$

References

• Course notes: AlgebraicCombinatorics/tex/FPS/Notations.tex

Tags

combinatorics, binomial coefficients, generating functions, Fibonacci, Catalan

Basic Combinatorial Principles

These are standard results in Mathlib. We provide docstrings explaining the combinatorial interpretations.

theorem AlgebraicCombinatorics.FPS.addition_principle {α : Type u_1} [DecidableEq α] (A B : Finset α) (h : Disjoint A B) : (A ∪ B).card = A.card + B.card

Addition Principle (Sum Rule): If $A$ and $B$ are disjoint finite sets, then $|A \cup B| = |A| + |B|$.

This is Finset.card_union_of_disjoint in Mathlib.

theorem AlgebraicCombinatorics.FPS.multiplication_principle {α : Type u_1} {β : Type u_2} (A : Finset α) (B : Finset β) : (A ×ˢ B).card = A.card * B.card

Multiplication Principle (Product Rule): If $A$ and $B$ are finite sets, then $|A \times B| = |A| \cdot |B|$.

This is Finset.card_product in Mathlib.

theorem AlgebraicCombinatorics.FPS.bijection_principle {α : Type u_1} {β : Type u_2} (A : Finset α) (B : Finset β) (e : α → β) (he : Function.Bijective e) (hst : ∀ (i : α), i ∈ A ↔ e i ∈ B) : A.card = B.card

Bijection Principle: If there is a bijection between two finite sets $X$ and $Y$, then $|X| = |Y|$.

This is Finset.card_bijective in Mathlib. The converse (equal cardinality implies existence of bijection) is Fintype.truncEquivFinOfCardEq.

theorem AlgebraicCombinatorics.FPS.card_subsets {α : Type u_1} (A : Finset α) : A.powerset.card = 2 ^ A.card

A set with $n$ elements has $2^n$ subsets.

This is Finset.card_powerset in Mathlib.

theorem AlgebraicCombinatorics.FPS.card_subsets_of_size {α : Type u_1} (A : Finset α) (k : ℕ) : (Finset.powersetCard k A).card = A.card.choose k

A set with $n$ elements has $\binom{n}{k}$ subsets of size $k$.

This is Finset.card_powersetCard in Mathlib.

Binomial Coefficients

The binomial coefficient $\binom{n}{k}$ is defined in Mathlib as Nat.choose for natural numbers and Ring.choose for more general rings.

Definition \ref{def.binom.binom}

For any numbers $n$ and $k$: $$\binom{n}{k} = \begin{cases} \frac{n(n-1)(n-2)\cdots(n-k+1)}{k!} & \text{if } k \in \mathbb{N} \\ 0 & \text{else} \end{cases}$$

In Mathlib, this is implemented as:

• Nat.choose n k for natural numbers $n, k$
• Ring.choose r n for elements $r$ in a binomial ring and $n \in \mathbb{N}$

The key identity relating Ring.choose to the textbook definition is: $$n! \cdot \binom{r}{n} = r(r-1)(r-2)\cdots(r-n+1)$$ which is the descending factorial (descending Pochhammer symbol).

theorem AlgebraicCombinatorics.FPS.binom_def_formula {K : Type u_1} [Field K] [CharZero K] (r : K) (n : ℕ) : Ring.choose r n = (descPochhammer ℤ n).smeval r / ↑n.factorial

Definition \ref{def.binom.binom} (Binomial Coefficient Formula): For any element $r$ in a field of characteristic zero and $n \in \mathbb{N}$, $$\binom{r}{n} = \frac{r(r-1)(r-2)\cdots(r-n+1)}{n!}$$

This is the fundamental definition of the binomial coefficient. In Mathlib, this is expressed using the descending Pochhammer symbol: (descPochhammer ℤ n).smeval r = n.factorial • Ring.choose r n

For fields of characteristic zero, we can write this as a division.

theorem AlgebraicCombinatorics.FPS.descPochhammer_eq_descFactorial (n k : ℕ) : (descPochhammer ℤ k).smeval ↑n = ↑(n.descFactorial k)

The descending Pochhammer symbol (descPochhammer ℤ n).smeval r equals the descending factorial $r(r-1)(r-2)\cdots(r-n+1)$.

This is the "falling factorial" or "descending factorial" notation often written as $(r)_n$ or $r^{\underline{n}}$ in combinatorics.

For natural numbers, this equals Nat.descFactorial.

theorem AlgebraicCombinatorics.FPS.binom_factorial_smul {R : Type u_1} [CommRing R] [BinomialRing R] [NatPowAssoc R] (r : R) (n : ℕ) : n.factorial • Ring.choose r n = (descPochhammer ℤ n).smeval r

The binomial coefficient satisfies the factorial formula: $$n! \cdot \binom{r}{n} = r(r-1)(r-2)\cdots(r-n+1)$$

This is Ring.descPochhammer_eq_factorial_smul_choose in Mathlib.

theorem AlgebraicCombinatorics.FPS.binom_natCast {R : Type u_1} [CommRing R] [BinomialRing R] [NatPowAssoc R] (n k : ℕ) : Ring.choose (↑n) k = ↑(n.choose k)

For natural numbers, Ring.choose agrees with Nat.choose: $$\binom{n}{k} = \text{Nat.choose } n\, k$$

This is Ring.choose_natCast in Mathlib.

theorem AlgebraicCombinatorics.FPS.binom_zero_right {R : Type u_1} [CommRing R] [BinomialRing R] [NatPowAssoc R] (r : R) : Ring.choose r 0 = 1

Base case: $\binom{r}{0} = 1$ for any $r$.

This follows from the definition: the empty product $r(r-1)\cdots(r-0+1)$ equals $1$.

theorem AlgebraicCombinatorics.FPS.binom_zero_left_pos {R : Type u_1} [CommRing R] [BinomialRing R] [NatPowAssoc R] {k : ℕ} (hk : 0 < k) : Ring.choose 0 k = 0

For $k > 0$, we have $\binom{0}{k} = 0$.

This follows from the definition: the product $0 \cdot (-1) \cdot (-2) \cdots$ has a factor of $0$.

theorem AlgebraicCombinatorics.FPS.binom_one_right {R : Type u_1} [CommRing R] [BinomialRing R] [NatPowAssoc R] (r : R) : Ring.choose r 1 = r

First case: $\binom{r}{1} = r$.

This follows from the definition: $\frac{r}{1!} = r$.

theorem AlgebraicCombinatorics.FPS.binom_neg_one (k : ℕ) : Ring.choose (-1) k = (-1) ^ k

Example \ref{exa.binom.-1choosek}: For any $k \in \mathbb{N}$, $\binom{-1}{k} = (-1)^k$.

theorem AlgebraicCombinatorics.FPS.binom_factorial_formula {n k : ℕ} (h : k ≤ n) : n.choose k = n.factorial / (k.factorial * (n - k).factorial)

The factorial formula for binomial coefficients: For $n, k \in \mathbb{N}$ with $k \leq n$, $$\binom{n}{k} = \frac{n!}{k!(n-k)!}$$

This is Nat.choose_eq_factorial_div_factorial in Mathlib (Equation \eqref{eq.binom.fac-form}).

theorem AlgebraicCombinatorics.FPS.prod_odd_eq_doubleFactorial (n : ℕ) : ∏ i ∈ Finset.range n, (2 * i + 1) = (2 * n - 1).doubleFactorial

The product of odd numbers 1·3·5·...·(2n-1) equals the double factorial (2n-1)‼.

theorem AlgebraicCombinatorics.FPS.factorial_dvd_prod_odd_mul_pow (n : ℕ) : n.factorial ∣ (∏ i ∈ Finset.range n, (2 * i + 1)) * 2 ^ n

n! divides the product (1·3·5·...·(2n-1)) · 2^n.

theorem AlgebraicCombinatorics.FPS.binom_two_n_n_eq (n : ℕ) : (2 * n).choose n = (∏ i ∈ Finset.range n, (2 * i + 1)) * 2 ^ n / n.factorial

Example \ref{exa.binom.2n-choose-n}: For $n \in \mathbb{N}$, $$\binom{2n}{n} = \frac{1 \cdot 3 \cdot 5 \cdots (2n-1)}{n!} \cdot 2^n$$

This relates the central binomial coefficient to double factorials.

theorem AlgebraicCombinatorics.FPS.pascal_identity (m n : ℕ) (hn : 0 < n) (hm : 0 < m) : m.choose n = (m - 1).choose (n - 1) + (m - 1).choose n

Proposition \ref{prop.binom.rec} (Pascal's Identity) for natural numbers: $$\binom{m}{n} = \binom{m-1}{n-1} + \binom{m-1}{n}$$

This is the fundamental recurrence for binomial coefficients. Note: For natural numbers, we need $m > 0$ because when $m = 0$ and $n = 1$, the LHS is $\binom{0}{1} = 0$ but the RHS (with Nat subtraction) becomes $\binom{0}{0} + \binom{0}{1} = 1 + 0 = 1$.

This is Nat.choose_eq_choose_pred_add in Mathlib.

theorem AlgebraicCombinatorics.FPS.pascal_identity_ring {R : Type u_1} [CommRing R] [BinomialRing R] [NatPowAssoc R] (m : R) (n : ℕ) (hn : 0 < n) : Ring.choose m n = Ring.choose (m - 1) (n - 1) + Ring.choose (m - 1) n

Proposition \ref{prop.binom.rec} (Pascal's Identity) for generalized binomial coefficients: $$\binom{m}{n} = \binom{m-1}{n-1} + \binom{m-1}{n}$$

This version works for any element $m$ in a binomial ring and any positive natural number $n$. This is Ring.choose_succ_succ in Mathlib, rewritten in the form matching the TeX source.

theorem AlgebraicCombinatorics.FPS.pascal_identity_succ {R : Type u_1} [CommRing R] [BinomialRing R] [NatPowAssoc R] (r : R) (k : ℕ) : Ring.choose (r + 1) (k + 1) = Ring.choose r k + Ring.choose r (k + 1)

Proposition \ref{prop.binom.rec} (Pascal's Identity) in the "successor" form: $$\binom{r+1}{k+1} = \binom{r}{k} + \binom{r}{k+1}$$

This is the fundamental recurrence for generalized binomial coefficients. This is Ring.choose_succ_succ in Mathlib.

theorem AlgebraicCombinatorics.FPS.pascal_identity_int (m : ℤ) (n : ℕ) (hn : 0 < n) : Ring.choose m n = Ring.choose (m - 1) (n - 1) + Ring.choose (m - 1) n

Pascal's identity for integers: $$\binom{m}{n} = \binom{m-1}{n-1} + \binom{m-1}{n}$$

This is a special case of pascal_identity_ring for the integers.

theorem AlgebraicCombinatorics.FPS.pascal_identity_rat (m : ℚ) (n : ℕ) (hn : 0 < n) : Ring.choose m n = Ring.choose (m - 1) (n - 1) + Ring.choose (m - 1) n

Pascal's identity for rationals: $$\binom{m}{n} = \binom{m-1}{n-1} + \binom{m-1}{n}$$

This is a special case of pascal_identity_ring for the rationals.

theorem AlgebraicCombinatorics.FPS.binom_zero_of_lt {m n : ℕ} (h : m < n) : m.choose n = 0

Proposition \ref{prop.binom.0}: Let $m, n \in \mathbb{N}$ with $m < n$. Then $\binom{m}{n} = 0$.

This is Nat.choose_eq_zero_of_lt in Mathlib.

theorem AlgebraicCombinatorics.FPS.binom_symm {n k : ℕ} (h : k ≤ n) : n.choose k = n.choose (n - k)

Theorem \ref{thm.binom.sym} (Symmetry of Binomial Coefficients): Let $n \in \mathbb{N}$ and $k \in \mathbb{R}$. Then $\binom{n}{k} = \binom{n}{n-k}$.

For natural numbers $k \leq n$, this is Nat.choose_symm.

@[simp]

theorem AlgebraicCombinatorics.FPS.binom_symm_add (a b : ℕ) : (a + b).choose a = (a + b).choose b

Symmetry of binomial coefficients when $n = a + b$. This is a useful variant: $\binom{a+b}{a} = \binom{a+b}{b}$.

theorem AlgebraicCombinatorics.FPS.binom_symm_of_eq_add {n a b : ℕ} (h : n = a + b) : n.choose a = n.choose b

Symmetry of binomial coefficients: if $n = a + b$, then $\binom{n}{a} = \binom{n}{b}$.

theorem AlgebraicCombinatorics.FPS.binom_symm_ring {R : Type u_1} [CommRing R] [BinomialRing R] [NatPowAssoc R] (n k : ℕ) (h : k ≤ n) : Ring.choose (↑n) k = Ring.choose (↑n) (n - k)

Symmetry of generalized binomial coefficients for Ring.choose when the first argument is a natural number. This extends binom_symm to binomial rings.

The Fibonacci Sequence (Example 1)

The Fibonacci sequence $(f_0, f_1, f_2, \ldots)$ is defined by:

• $f_0 = 0$
• $f_1 = 1$
• $f_n = f_{n-1} + f_{n-2}$ for $n \geq 2$

Its generating function is $F(x) = \sum_{n \geq 0} f_n x^n = \frac{x}{1-x-x^2}$.

Mathlib equivalences: The Fibonacci sequence is Nat.fib in Mathlib. The golden ratios are Real.goldenRatio and Real.goldenConj in Mathlib.NumberTheory.Real.GoldenRatio. Binet's formula is proved there as Real.coe_fib_eq.

def AlgebraicCombinatorics.FPS.fibonacci : ℕ → ℕ

The Fibonacci sequence.

Mathlib note: This is definitionally equal to Nat.fib in Mathlib.

Equations

• AlgebraicCombinatorics.FPS.fibonacci = Nat.fib

theorem AlgebraicCombinatorics.FPS.fibonacci_eq_nat_fib (n : ℕ) : fibonacci n = Nat.fib n

Our definition of fibonacci is definitionally equal to Nat.fib.

noncomputable def AlgebraicCombinatorics.FPS.goldenRatioPlus : ℝ

The golden ratio $\phi_+ = \frac{1 + \sqrt{5}}{2}$.

Mathlib note: This is equal to Real.goldenRatio in Mathlib.

Equations

• AlgebraicCombinatorics.FPS.goldenRatioPlus = (1 + √5) / 2

noncomputable def AlgebraicCombinatorics.FPS.goldenRatioMinus : ℝ

The conjugate golden ratio $\phi_- = \frac{1 - \sqrt{5}}{2}$.

Mathlib note: This is equal to Real.goldenConj in Mathlib.

Equations

• AlgebraicCombinatorics.FPS.goldenRatioMinus = (1 - √5) / 2

theorem AlgebraicCombinatorics.FPS.goldenRatioPlus_eq : goldenRatioPlus = Real.goldenRatio

Our goldenRatioPlus equals Mathlib's Real.goldenRatio.

theorem AlgebraicCombinatorics.FPS.goldenRatioMinus_eq : goldenRatioMinus = Real.goldenConj

Our goldenRatioMinus equals Mathlib's Real.goldenConj.

theorem AlgebraicCombinatorics.FPS.fibonacci_gf : (PowerSeries.mk fun (n : ℕ) => ↑(fibonacci n)) = PowerSeries.X * (1 - PowerSeries.X - PowerSeries.X ^ 2)⁻¹

The generating function of the Fibonacci sequence is $\frac{x}{1-x-x^2}$.

Equation \eqref{eq.sec.gf.exas.1.Fx=1}.

theorem AlgebraicCombinatorics.FPS.fibonacci_binet (n : ℕ) : ↑(fibonacci n) = (goldenRatioPlus ^ n - goldenRatioMinus ^ n) / √5

Binet's Formula: For any $n \in \mathbb{N}$, $$f_n = \frac{1}{\sqrt{5}} \left( \phi_+^n - \phi_-^n \right)$$ where $\phi_\pm = \frac{1 \pm \sqrt{5}}{2}$ are the golden ratios.

Mathlib note: This is proved as Real.coe_fib_eq in Mathlib.

Dyck Words and Catalan Numbers (Example 2)

A Dyck word of length $2n$ is a $2n$-tuple of $0$s and $1$s such that:

1. There are exactly $n$ zeros and $n$ ones
2. For each prefix, the number of $0$s does not exceed the number of $1$s

The Catalan numbers $c_n$ count Dyck words of length $2n$.

Mathlib equivalences:

• Catalan numbers are defined in Mathlib.Combinatorics.Enumerative.Catalan as Nat.catalan using the recurrence relation. The explicit formula catalan n = centralBinom n / (n + 1) is proved as Nat.catalan_eq_centralBinom_div.
• Dyck words are formalized in Mathlib.Combinatorics.Enumerative.DyckWord as the DyckWord structure using a DyckStep enum (U for up, D for down) rather than Bool.

def AlgebraicCombinatorics.FPS.isDyckWord (w : List Bool) : Prop

A list is a Dyck word if it consists of 0s and 1s, has equal numbers of each, and every prefix has at least as many 1s as 0s.

Here we represent 1 as true and 0 as false.

Mathlib note: This is an alternative representation to Mathlib's DyckWord structure, which uses a DyckStep enum with constructors U (up) and D (down). The two representations are equivalent via the bijection sending true to U and false to D.

Equations

• AlgebraicCombinatorics.FPS.isDyckWord w = (List.count true w = List.count false w ∧ ∀ k ≤ w.length, List.count false (List.take k w) ≤ List.count true (List.take k w))

def AlgebraicCombinatorics.FPS.catalan (n : ℕ) : ℕ

The Catalan numbers, defined as $c_n = \frac{1}{n+1}\binom{2n}{n}$.

Mathlib note: This is equivalent to Mathlib's catalan, which is defined recursively. The equivalence is proved by catalan_eq_mathlib_catalan.

Equations

• AlgebraicCombinatorics.FPS.catalan n = (2 * n).choose n / (n + 1)

theorem AlgebraicCombinatorics.FPS.catalan_eq_mathlib_catalan (n : ℕ) : catalan n = _root_.catalan n

Our explicit definition of catalan equals Mathlib's recursive catalan.

This follows from catalan_eq_centralBinom_div in Mathlib.

@[simp]

theorem AlgebraicCombinatorics.FPS.catalan_zero : catalan 0 = 1

First few Catalan numbers: $c_0 = 1$.

@[simp]

theorem AlgebraicCombinatorics.FPS.catalan_one : catalan 1 = 1

First few Catalan numbers: $c_1 = 1$.

@[simp]

theorem AlgebraicCombinatorics.FPS.catalan_two : catalan 2 = 2

First few Catalan numbers: $c_2 = 2$.

@[simp]

theorem AlgebraicCombinatorics.FPS.catalan_three : catalan 3 = 5

First few Catalan numbers: $c_3 = 5$.

theorem AlgebraicCombinatorics.FPS.catalan_recurrence (n : ℕ) (hn : 0 < n) : catalan n = ∑ k ∈ Finset.range n, catalan k * catalan (n - 1 - k)

The Catalan recurrence relation: $$c_n = \sum_{k=0}^{n-1} c_k c_{n-1-k}$$ for $n \geq 1$, with $c_0 = 1$.

theorem AlgebraicCombinatorics.FPS.catalan_explicit (n : ℕ) : catalan n = (2 * n).choose n / (n + 1)

Equation \eqref{eq.sec.gf.exas.cn=1/(n+1)}: The explicit formula for Catalan numbers: $$c_n = \frac{1}{n+1} \binom{2n}{n}$$

theorem AlgebraicCombinatorics.FPS.catalan_as_diff {n : ℕ} (hn : 0 < n) : catalan n = (2 * n).choose n - (2 * n).choose (n - 1)

Equation \eqref{eq.sec.gf.exas.cn=diff}: Alternative form of Catalan numbers: $$c_n = \binom{2n}{n} - \binom{2n}{n-1}$$

Note: For $n = 0$, this becomes $1 - \binom{0}{-1} = 1 - 0 = 1$, which is correct since $\binom{m}{k} = 0$ when $k < 0$ (or equivalently, when $k$ is not a natural number). In Lean's Nat.choose, we have 0.choose (0 - 1) = 0.choose 0 = 1 due to subtraction truncation, so this theorem requires $n > 0$.

theorem AlgebraicCombinatorics.FPS.catalan_gf_equation : have C := PowerSeries.mk fun (n : ℕ) => ↑(catalan n); C = 1 + PowerSeries.X * C ^ 2

The generating function of the Catalan numbers satisfies $C(x) = 1 + x \cdot C(x)^2$.

theorem AlgebraicCombinatorics.FPS.choose_half_recurrence (n : ℕ) : (↑n + 1) * Ring.choose (1 / 2) (n + 1) = (1 / 2 - ↑n) * Ring.choose (1 / 2) n

Recurrence relation for Ring.choose at 1/2: $(n + 1) \cdot \binom{1/2}{n+1} = (1/2 - n) \cdot \binom{1/2}{n}$.

This follows from the descending Pochhammer formula for binomial coefficients.

theorem AlgebraicCombinatorics.FPS.A_eq_neg_two_centralBinom (n : ℕ) : Ring.choose (1 / 2) (n + 1) * (-4) ^ (n + 1) * (↑n + 1) = -2 * ↑n.centralBinom

Key identity: $\binom{1/2}{n+1} \cdot (-4)^{n+1} \cdot (n+1) = -2 \cdot \binom{2n}{n}$.

This relates the binomial coefficient at 1/2 to the central binomial coefficient.

theorem AlgebraicCombinatorics.FPS.choose_half_neg4_pow_eq (n : ℕ) : Ring.choose (1 / 2) (n + 1) * (-4) ^ (n + 1) = -2 * ↑(catalan n)

The key coefficient identity for the Catalan generating function: $\binom{1/2}{n+1} \cdot (-4)^{n+1} = -2 \cdot c_n$.

theorem AlgebraicCombinatorics.FPS.catalan_gf_explicit : 2 • ((PowerSeries.mk fun (n : ℕ) => ↑(catalan n)) * PowerSeries.X) = 1 - PowerSeries.mk fun (n : ℕ) => Ring.choose (1 / 2) n * (-4) ^ n

The generating function of the Catalan numbers is related to $\sqrt{1 - 4x}$.

The exact formula $C(x) = \frac{1 - \sqrt{1 - 4x}}{2x}$ is reformulated as $2x \cdot C(x) = 1 - \sqrt{1 - 4x}$ to avoid division by $x$ in power series (since $x$ is not a unit in the ring of formal power series).

The square root $\sqrt{1 - 4x}$ is represented by the binomial series $\sum_{n \geq 0} \binom{1/2}{n} (-4x)^n = \sum_{n \geq 0} \binom{1/2}{n} (-4)^n x^n$.

Equation \eqref{eq.sec.gf.exas.2.-}.

The Vandermonde Convolution (Example 3)

The Vandermonde convolution identity (also called Chu-Vandermonde): $$\binom{a+b}{n} = \sum_{k=0}^{n} \binom{a}{k} \binom{b}{n-k}$$

theorem AlgebraicCombinatorics.FPS.vandermonde_convolution (a b n : ℕ) : (a + b).choose n = ∑ k ∈ Finset.range (n + 1), a.choose k * b.choose (n - k)

The Vandermonde convolution identity: $$\binom{a+b}{n} = \sum_{k=0}^{n} \binom{a}{k} \binom{b}{n-k}$$

Mathlib note: Mathlib's Nat.add_choose_eq uses ∑ ij ∈ antidiagonal n instead of ∑ k ∈ range (n + 1). The two formulations are equivalent via Finset.sum_antidiagonal_eq_sum_range_succ_mk. This version matches the source material.

Solving a Recurrence (Example 4)

Consider the sequence $(a_0, a_1, a_2, \ldots)$ defined by:

• $a_0 = 1$
• $a_{n+1} = 2a_n + n$ for all $n \geq 0$

Using generating functions, we can show that $a_n = 2^{n+1} - (n+1)$.

def AlgebraicCombinatorics.FPS.exampleRecurrence : ℕ → ℕ

The sequence defined by $a_0 = 1$ and $a_{n+1} = 2a_n + n$.

Equations

• AlgebraicCombinatorics.FPS.exampleRecurrence 0 = 1
• AlgebraicCombinatorics.FPS.exampleRecurrence n.succ = 2 * AlgebraicCombinatorics.FPS.exampleRecurrence n + n

@[simp]

theorem AlgebraicCombinatorics.FPS.exampleRecurrence_zero : exampleRecurrence 0 = 1

First few values: $a_0 = 1$.

@[simp]

theorem AlgebraicCombinatorics.FPS.exampleRecurrence_one : exampleRecurrence 1 = 2

First few values: $a_1 = 2$.

@[simp]

theorem AlgebraicCombinatorics.FPS.exampleRecurrence_two : exampleRecurrence 2 = 5

First few values: $a_2 = 5$.

theorem AlgebraicCombinatorics.FPS.exampleRecurrence_explicit (n : ℕ) : exampleRecurrence n = 2 ^ (n + 1) - (n + 1)

The explicit formula: $a_n = 2^{n+1} - (n+1)$.

Auxiliary Generating Function Results

These are helper results about power series used in the examples above.

theorem AlgebraicCombinatorics.FPS.geometric_series : (1 - PowerSeries.X)⁻¹ = PowerSeries.mk fun (x : ℕ) => 1

The geometric series: $\frac{1}{1-x} = 1 + x + x^2 + x^3 + \cdots$

Equation \eqref{eq.sec.gf.exas.1.1/1-x}.

theorem AlgebraicCombinatorics.FPS.geometric_series_scaled (α : ℚ) : (1 - α • PowerSeries.X)⁻¹ = PowerSeries.mk fun (n : ℕ) => α ^ n

Generalized geometric series: $\frac{1}{1-\alpha x} = \sum_{k \geq 0} \alpha^k x^k$

Equation \eqref{eq.sec.gf.exas.1.1/1-ax}.

theorem AlgebraicCombinatorics.FPS.deriv_inv_one_minus_x : (PowerSeries.derivative ℚ) (1 - PowerSeries.X)⁻¹ = (1 - PowerSeries.X)⁻¹ ^ 2

The derivative of $\frac{1}{1-x}$ is $\frac{1}{(1-x)^2}$.

Equation \eqref{eq.sec.gf.exas.4.1/(1-x)2}.

theorem AlgebraicCombinatorics.FPS.sum_n_plus_one_pow : (PowerSeries.mk fun (n : ℕ) => ↑n + 1) = (1 - PowerSeries.X)⁻¹ ^ 2

The power series $\sum_{n \geq 0} (n+1) x^n = \frac{1}{(1-x)^2}$.

Equation \eqref{eq.sec.gf.exas.4.1/(1-x)2}.

theorem AlgebraicCombinatorics.FPS.sum_n_pow : (PowerSeries.mk fun (n : ℕ) => ↑n) = PowerSeries.X * (1 - PowerSeries.X)⁻¹ ^ 2

The power series $\sum_{n \geq 1} n x^n = \frac{x}{(1-x)^2}$.

Equation \eqref{eq.sec.gf.exas.4.x/(1-x)2}.