Dependencies

Let \(S \subseteq \{ 1, \ldots , n\} \) be a nonempty partition of \(n\) into different parts with base \(b\), slope \(s\), max \(m = \max (S)\), and slope set \(D\). We define:

\(\alpha \): For \(S \in \mathcal{P}_\alpha (n)\) (equivalently, \(b \leq s\) and \(b \notin D\), or \(b \leq s - 1\)):

\(\beta \): For \(S \in \mathcal{P}_\beta (n)\) (equivalently, \(b {\gt} s\) and \(b \notin D\), or \(b \geq s + 2\)):

Consider a nonempty partition \(S \subseteq \{ 1, \ldots , n\} \) of \(n\) into different parts. We define the base \(b \in S\) as the smallest element of the partition, \(b = \min (S)\). Let \(\max (S)\) denote the largest element of \(S\). We define the slope \(s\) as:

and the slope set \(D\) as \(\{ \max (S), \max (S)-1, \ldots , \max (S)-s + 1\} \).

Let \(n \in \mathbb {N}\). We define the following sets of partitions of \(n\) into distinct positive parts:

We further define the number of even and odd partitions of \(n\) as \(p_e(n) = |\mathcal{P}_{\mathrm{even}}(n)|\) and \(p_o(n) = |\mathcal{P}_{\mathrm{odd}}(n)|\).

Let \(A = \texttt{LaurentPolynomial}\, \mathbb {C}\), \(z = T(1)\), \(z^{-1} = T(-1)\) viewed as constant power series in \(A[\! [ X]\! ]\). Define:

Here \(T(k)\) is the degree-\(k\) monomial in the Laurent polynomial ring \(A\), so \(T(n) = z^n\) and \(T(-(m+1)) = z^{-(m+1)}\).

For \(a \in R[\! [ X]\! ]\) and \(n \in \mathbb {N}\),

For \(k \in \mathbb {N}\), define

\(\mathrm{jacobiProd}(q,z) := (q;q)_\infty \, (-z;q)_\infty \, (-q/z;q)_\infty \), and the bilateral series \(\mathrm{jacobiBilateral}(q,z) := \sum _{k\ge 0} z^k q^{\binom {k}{2}} + \sum _{m\ge 0} z^{-(m+1)} q^{\binom {m+2}{2}}\) (the non-negative and negative halves of \(\sum _{k\in \mathbb {Z}} z^k q^{k(k-1)/2}\)).

Let \(n \in \mathbb {N}_{\geq 1}\) be a positive integer. Consider \(S \in \mathcal{P}(n)\) nonempty with base \(b\), slope \(s\), and slope set \(D\). We define the following sets of partitions of \(n\) into distinct positive parts:

By convention \(\emptyset \in \mathcal{P}_{\mathrm{special}}(0)\) (and \(\mathcal{P}(0) = \{ \emptyset \} \)).

A partition of a positive integer \(n\), also called an integer partition, is a way of writing \(n\) as a sum of positive integers. Two sums that differ only in the order of their summands are considered the same partition.

The partition function \(p(n)\) represents the number of possible partitions of a natural number \(n\).

\(\omega (k) := \bigl(k(3k-1)/2\bigr)\) for \(k \in \mathbb {Z}\) (the product \(k(3k-1)\) is always even), realised in Lean as a natural number.

The Gaussian binomial coefficient \(\binom {n}{k}_q \in R\) is defined by recursion on \(n\) and \(k\):

This is the \(q\)-Pascal recurrence in the form stated in Lemma 25 (with the index shift \(k \mapsto k+1\)). By construction \(\binom {n}{k}_q\) is a polynomial in \(q\) with integer coefficients, defined for every pair \((n, k) \in \mathbb {N}^2\) (no division, no roots-of-unity exclusion).

For \(n \in \mathbb {N}\), the finite \(q\)-Pochhammer symbol is

In Lean, this is implemented as \(\prod \) k \(\in \) Finset.range n, (1 - a * q^k), specialising to \((a; q)_0 = 1\) (the empty product).

defined unconditionally via tprod. The value is mathematically meaningful (and the product is convergent) under the hypothesis \(\| q\| {\lt} 1\) provided by Lemma 34.

For \(\| q\| {\lt} 1\) and \(k \in \mathbb {N}\), \(S_k(q) := \sum _{m \ge 0} q^{m(m+k)} / \bigl((q;q)_m\, (q;q)_{m+k}\bigr)\).

For \(k \in \mathbb {N}_{\geq 1}\) define \( S_{-k}=\{ k, k+1, \ldots , 2k-1\} \) (a set of \(k\) elements summing to \((3k^2-k)/2\)).
For \(k\in \mathbb {N}_{\geq 1}\) define \(S_{k}=\{ k+1, k+2, \ldots , 2k\} \) (a set of \(k\) elements summing to \((3k^2+k)/2\)).

For \(\| q\| {\lt} 1\) and \(l \ge 0\),

For \(\| q\| {\lt} 1\) and \(k \ge 0\),

For \(\| q\| {\lt} 1\) and \(\| z\| {\lt} 1\),

For \(\| q\| {\lt} 1\) and \(\| z\| {\lt} 1\),

For \(\| q\| {\lt} 1\) and \(z \neq 0\) (no annulus condition),

For \(\| q\| {\lt} 1\), the series \(S(z) := \sum _n q^{\binom {n}{2}} z^n / (q;q)_n\) satisfies \(S(z) = (1+z)\, S(qz)\).

\([X^d]\, \texttt{qPochInf}\, a = [X^d]\, \texttt{qPoch}\, a\, (d+1)\).

If \(d {\lt} n\) then \([X^d]\, \texttt{qPoch}\, a\, (n+1) = [X^d]\, \texttt{qPoch}\, a\, n\).

The constant term of \(\texttt{qPoch}\, (X : R[\! [ X]\! ])\, n\) is \(1\).

If \(1 - [X^0]\, a\) is a unit of \(R\), then \(\texttt{qPochInf}\, a\) is a unit of \(R[\! [ X]\! ]\).

\(\texttt{qPoch}\, a\, (n+1) = (1-a)\cdot \texttt{qPoch}\, (aX)\, n\).

\(\texttt{qPoch}\, a\, (n+1) = \texttt{qPoch}\, a\, n \cdot (1 - a\cdot X^n)\).

\(\texttt{qPoch}\, a\, 0 = 1\).

For every \(n \in \mathbb {N}\): \(\texttt{qPochInf}\, a = \texttt{qPoch}\, a\, n \cdot \texttt{qPochInf}\, (a\cdot X^n)\).

\(\texttt{qPochInf}\, a = (1-a)\cdot \texttt{qPochInf}\, (a\cdot X)\).

In \(R[\! [ X]\! ]\):

For every \(k\):

The summand of \(S^{\mathrm{fps}}_k\) is summable in \(R[\! [ X]\! ]\).

For \(a, q \in \mathbb {C}\) with \(\| q\| {\lt} 1\), the family \(k \mapsto 1 - a\, q^k\) is multipliable; in particular the partial products converge to \((a; q)_\infty \).

For all \(k \leq n\),

If \(n {\lt} k\), then \(\binom {n}{k}_q = 0\).

\(\binom {n}{n}_q = 1\) for every \(n \in \mathbb {N}\).

For all \(n, k \in \mathbb {N}\),

(Equivalently, with \(k \geq 1\): \(\binom {n+1}{k}_q = \binom {n}{k}_q + q^{n - k + 1}\binom {n}{k-1}_q\). A symmetric form \(\binom {n+1}{k+1}_q = q^{k+1}\binom {n}{k+1}_q + \binom {n}{k}_q\) also holds; we use the first.)

For all \(n \in \mathbb {N}\),

\((a; q)_0 = 1\).

For \(\| q\| {\lt} 1\) and \(\| z\| {\lt} 1\),

For \(\| q\| {\lt} 1\) and every \(n\),

For \(\| q\| {\lt} 1\) and every \(k\),

For \(\| q\| {\lt} 1\), \(S_k(q) \to 1/(q;q)_\infty \) as \(k \to \infty \).

For \(\| q\| {\lt} 1\), the summand of \(S_k\) is summable.

The composition of maps \(\alpha \circ \beta \) is equal to the identity map on \(\mathcal{P}_\beta (n)\). Equivalently, if \(S\in \mathcal{P}_\beta (n)\) then \(\alpha (\beta (S))=S\).

The map \(\alpha : \mathcal{P}_\alpha (n)\to \mathcal{P}_\beta (n)\) is a bijection.
The map \(\beta : \mathcal{P}_\beta (n)\to \mathcal{P}_\alpha (n)\) is a bijection.

The operations \(\alpha \) and \(\beta \) change the parity of the number of parts of a partition. More precisely,

• If \(S\in \mathcal{P}_\alpha (n)\cap \mathcal{P}_{\mathrm{odd}}(n) \) then \(\alpha (S) \in \mathcal{P}_\beta (n)\cap \mathcal{P}_{\mathrm{even}}(n) \);

• If \(S\in \mathcal{P}_\alpha (n)\cap \mathcal{P}_{\mathrm{even}}(n) \) then \(\alpha (S) \in \mathcal{P}_\beta (n)\cap \mathcal{P}_{\mathrm{odd}}(n) \);

• If \(S\in \mathcal{P}_\beta (n)\cap \mathcal{P}_{\mathrm{odd}}(n) \) then \(\beta (S) \in \mathcal{P}_\alpha (n)\cap \mathcal{P}_{\mathrm{even}}(n) \);

• If \(S\in \mathcal{P}_\beta (n)\cap \mathcal{P}_{\mathrm{even}}(n) \) then \(\beta (S) \in \mathcal{P}_\alpha (n)\cap \mathcal{P}_{\mathrm{odd}}(n) \).

For all positive integer numbers \(n\) the following holds

For all positive natural numbers \(n\in \mathbb {N}_{\geq 1}\) the following holds: The sets \(\mathcal{P}_{\alpha }(n)\), \(\mathcal{P}_{\beta }(n)\), \(\mathcal{P}_{\mathrm{special}}(n)\) are pairwise disjoint.

If \(S\in \mathcal{P}_\alpha (n)\) then \(\alpha (S)\in \mathcal{P}_\beta (n)\).

The composition of maps \(\beta \circ \alpha \) is equal to the identity map on \(\mathcal{P}_\alpha (n)\). Equivalently, if \(S\in \mathcal{P}_\alpha (n)\) then \(\beta (\alpha (S))=S\).

If \(S\in \mathcal{P}_\beta (n)\) then \(\beta (S)\in \mathcal{P}_\alpha (n)\).

We have

where \(c_0=1\) and \(c_n=p_e(n)-p_o(n)\) for \(n\geq 1\).

The generating function for \(p(n)\) is given by

For \(n\in \mathbb {N}_{\geq 1}\):

• If \(n\) is not a pentagonal number, then \(\mathcal{P}_{\mathrm{special}}(n) = \emptyset \).

• If \(n = \frac{3k^2 - k}{2}\) for some \(k \in \mathbb {Z}_{\geq 1}\), then \(\mathcal{P}_{\mathrm{special}}(n) = \{ S_{-k}\} \).

• If \(n = \frac{3k^2 + k}{2}\) for some \(k \in \mathbb {Z}_{\geq 1}\), then \(\mathcal{P}_{\mathrm{special}}(n) = \{ S_{k}\} \).

For \(n = 0\), \(\mathcal{P}_{\mathrm{special}}(0) = \{ \emptyset \} \) by convention.

For \(\| q\| {\lt} 1\) and every \(z\in \mathbb {C}\),

For every \(l \ge 0\):

For every \(k \ge 0\):

That is, the \(k\)-th diagonal sum of the Cauchy product equals \(X^{\binom {k}{2}}\).

In \(R[\! [ X]\! ]\) (for any commutative ring \(R\) with discrete topology),

In \(A[\! [ X]\! ]\) (with \(A = \texttt{LaurentPolynomial}\, \mathbb {C}\)):

that is,

For every \(k\),

The family \(k \mapsto 1 - a\cdot X^k\) is multipliable in \(R[\! [ X]\! ]\) (with the pi / \(X\)-adic topology).

\(S^{\mathrm{fps}}_k = S^{\mathrm{fps}}_0\) for all \(k \in \mathbb {N}\).

For \(\| q\| {\lt} 1\), the partial products \(\prod _{k {\lt} N}(1 - q^{2k})(1 + zq^{2k-1})(1 + q^{2k-1}/z)\) converge locally uniformly on \(\{ z \neq 0\} \) to \(\mathrm{jacobiProd}(q,z)\).

For \(\| q\| {\lt} 1\), the bilateral partial sums \(\sum _{|k| {\lt} N} z^k\, q^{\binom {k}{2}}\) converge locally uniformly on \(\{ z \neq 0\} \) to \(\mathrm{jacobiBilateral}(q,z)\).

For \(\| q\| {\lt} 1\) and every \(z \neq 0\),

For \(\| q\| {\lt} 1\), \(\| z\| {\lt} 1\), \(z \neq 0\), \(\; \mathrm{jacobiProd}(q,z) = \mathrm{jacobiBilateral}(q,z)\); that is,

For \(\| q\| {\lt} 1\),

In \(\mathbb {Z}[q, z]\), for every \(n \geq 0\),

For \(|q| {\lt} 1\) and any \(a, z \in \mathbb {C}\) with \(|z| {\lt} 1\),

For \(a, z, q \in \mathbb {C}\) with \(\| q\| {\lt} 1\) and \(\| z\| {\lt} 1\),

(Equivalent to Theorem 24.) The Lean theorem is QSeries.hasSum_qPochhammer_div_mul_pow in QSeries/CauchyIdentity.lean (in Qseries_Aristotle_new). The proof realised in Lean follows Heine’s functional-equation argument spelled out in the proof of Theorem 24 above, organised under section CauchyIdentity: non-vanishing of \((z;q)_\infty \) (qPochhammerInf_z_q_ne_zero), the telescoping recursion \((z;q)_\infty = (1-z)\, (zq;q)_\infty \) (qPochhammerInf_recursion), the coefficient recurrence \(c_{n+1}(1-q^{n+1}) = c_n(1 - a q^n)\) (cauchyCoeff_succ_mul), the functional equations for \(F\) and \(G\) (cauchy_functional_eq_F, cauchy_functional_eq_G), iteration on the disc (iterated_functional_eq_disc), and the Tannery-based limit \(F(q^n z) \to 1\) (tendsto_F_qpow). The alternative route via a finite Cauchy-type analog of Theorem 23 is not formalised.

For \(\| q\| {\lt} 1\) and every \(k\), \(\; S_k(q) = 1/(q;q)_\infty \).

For \(\| q\| {\lt} 1\) and every \(z \in \mathbb {C}\), the non-negative part \(\sum _{k \ge 0} z^k\, q^{\binom {k}{2}}\) is summable.